law is_zero_to_nat

lawful-words@0.1.0.0 · proof_u32.bend:278

import Base

278law is_zero_to_nat:
279  for +a: U32
280  {U32.is_zero(a) == Nat.is_eq(U32.to_nat(a), 0n) : Bool}