law u32_to_from_nat

bend-kit-lemmas@0.1.1.0 · lemmas.bend:686

import Base
import bend-mathlib@0.7.4.0/nat.bend as MNat

686law u32_to_from_nat:
687  for k: Nat
688  for +h: MNat.lt(k, pow2(32n))
689  {U32.to_nat(U32.from_nat(k)) == k : Nat}