law ed48

lawful-fields@0.1.1.0 · proof_num.bend:206

import Base

206law ed48:
207  for +x: U32
208  for +hge: {U32.is_ge(x, 48) == True{} : Bool}
209  {U32.to_nat(U32.sub(x, 48)) == Nat.sub(U32.to_nat(x), 48n) : Nat}