law u32_from_nat_to_nat

bend-mathlib@0.8.1.0 · u32.bend:710

import Base

710# Converting a U32 to a natural and back is the identity: from_nat (to_nat a) = a.
711law u32_from_nat_to_nat:
712  for a: U32
713  {U32.from_nat(U32.to_nat(a)) == a : U32}