def nz

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/u32laws.bend:140

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/generic.bend as SG

140def nz(+b: U32, +h: {Nat.is_eq(SG.u32_val(b), 0n) == False{} : Bool}) -> {U32.is_zero(b) == False{} : Bool}:
141  Equal.trans(Bool, U32.is_zero(b), Nat.is_eq(v(b), 0n), False{}, zero_nat(b), h)