law to_nat_lt_p

lawful-words@0.1.0.0 · proof_u32.bend:126

import Base

126law to_nat_lt_p:
127  for +a: U32
128  {Nat.is_lt(U32.to_nat(a), Nat.pow(2n, 32n)) == True{} : Bool}