law to_nat_from_nat

lawful-words@0.1.0.0 · LAWS.bend:32

import Base

32law to_nat_from_nat:
33  for n: Nat
34  {U32.to_nat(U32.from_nat(n)) == Nat.mod(n, Nat.pow(2n, 32n)) : Nat}