def ssub

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix32.bend:131

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

131def ssub(+a: U32, +b: U32, +c: Bool, +hn: {Nat.is_lt(SG.u32_val(a), SG.u32_val(b)) == c : Bool}) -> {SG.u32_val(F.pick(U32, c, 0, U32.sub(a, b))) == Nat.sub(SG.u32_val(a), SG.u32_val(b)) : Nat}:
132  match c:
133    case True{}:
134      Equal.sym(Nat, Nat.sub(SG.u32_val(a), SG.u32_val(b)), 0n, sub_big(SG.u32_val(a), SG.u32_val(b), N.lt_le(SG.u32_val(a), SG.u32_val(b), hn)))
135    case False{}:
136      sub_exact(a, b, N.not_lt_le(SG.u32_val(a), SG.u32_val(b), hn))