law lt10

lawful-fields@0.1.1.0 · proof_digits.bend:436

import Base

436law lt10:
437  for +n: U32
438  for +hs: {U32.is_lt(n, 10) == True{} : Bool}
439  {Nat.is_lt(U32.to_nat(n), 10n) == True{} : Bool}