def sub_exact
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix32.bend:109
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32.bend as Fix32
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/proofs/math/typed/u32laws.bend as LW
109def sub_exact(+a: U32, +b: U32, +h: {Nat.is_le(SG.u32_val(b), SG.u32_val(a)) == True{} : Bool}) -> {SG.u32_val(U32.sub(a, b)) == Nat.sub(SG.u32_val(a), SG.u32_val(b)) : Nat}:
110 LW.ops_sub(a, b, h)