law to_nat_from_nat_p

lawful-words@0.1.0.0 · proof_u32.bend:192

import Base

192law to_nat_from_nat_p:
193  for +n: Nat
194  {U32.to_nat(U32.from_nat(n)) == Nat.mod(n, Nat.pow(2n, 32n)) : Nat}