def bq.add_sub

bend-osdev-algo@0.1.0.0 · proof_bsearch.bend:280

import Base
import bend-osdev-algo@0.1.0.0/proof_u32.bend as U

280def bq.add_sub(d: Nat, s: Nat, e: {Nat.is_le(d, s) == True{} : Bool}) -> {Nat.add(d, Nat.sub(s, d)) == s : Nat}:
281  match d s:
282    case 0n +ss:
283      bq.sub_zero(ss)
284    case 1n+dp 0n:
285      Empty.absurd({1n+Nat.add(dp, 0n) == 0n : Nat}, bq.ft(e))
286    case 1n+ +dp 1n+ +sp:
287      U.uq.succ_cong(Nat.add(dp, Nat.sub(sp, dp)), sp, bq.add_sub(dp, sp, e))