law u32_from_nat_to_nat_sym

bend-mathlib@0.8.1.0 · u32.bend:1227

import Base

1227# Converting a U32 to a natural and back is the identity: from_nat (to_nat a) = a, reversed to rewrite toward the simple side.
1228law u32_from_nat_to_nat_sym:
1229  for a: U32
1230  {a == U32.from_nat(U32.to_nat(a)) : U32}