law to_nat_from_nat.m

lawful-words@0.1.0.0 · proof_u32.bend:174

import Base

174law to_nat_from_nat.m:
175  for +n: Nat
176  for +m: Nat
177  for +hm: {Nat.pow(2n, 32n) == m : Nat}
178  {U32.to_nat(U32.from_nat(n)) == Nat.mod(n, m) : Nat}