def zero_nat
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as Shrnimport Base
141def zero_nat(+a: U32) -> {U32.is_zero(a) == Nat.is_eq(v(a), 0n) : Bool}:
142 is_zero_c(a, U32.is_zero(a), {==}, v(a), {==})
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as Shrnimport Base
141def zero_nat(+a: U32) -> {U32.is_zero(a) == Nat.is_eq(v(a), 0n) : Bool}:
142 is_zero_c(a, U32.is_zero(a), {==}, v(a), {==})