def hi_zero
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32laws.bend:235
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as U32laws
import Base
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
235def hi_zero(+a: U32, +b: U32, +h: {I.u32_is(NM.MulOver{a, b}) == False{} : Bool}) -> {v(X.hi(X.mul32(a, b))) == 0n : Nat}:
236 +z = not_false(U32.is_zero(X.hi(X.mul32(a, b))), h)
237 N.eq_from_is_eq(v(X.hi(X.mul32(a, b))), 0n, Equal.trans(Bool, Nat.is_eq(v(X.hi(X.mul32(a, b))), 0n), U32.is_zero(X.hi(X.mul32(a, b))), True{}, Equal.sym(Bool, U32.is_zero(X.hi(X.mul32(a, b))), Nat.is_eq(v(X.hi(X.mul32(a, b))), 0n), zero_nat(X.hi(X.mul32(a, b)))), z))