law k9

lawful-fields@0.1.1.0 · proof_num.bend:214

import Base

214law k9:
215  for +x: U32
216  for +hle: {U32.is_le(x, 57) == True{} : Bool}
217  {Nat.is_le(Nat.sub(U32.to_nat(x), 48n), 9n) == True{} : Bool}