law roundtrip

stelliferous@0.0.2.0 · proofs/nat_to_u32_bounds.bend:71

import Base

71law roundtrip:
72  for +n: Nat
73  for +cap: U32
74  for +cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool}
75  for h: {Nat.is_le(n,U32.to_nat(cap)) == True{} : Bool}
76  {U32.to_nat(U32.from_nat(n)) == n : Nat}