U32laws.nz: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend as U32laws
Lines 140-141 of bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend&start_line=140&end_line=141

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

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

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend&name=zero_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/generic.bend&name=u32_val