law dg_small_n

lawful-fields@0.1.1.0 · proof_digits.bend:454

import Base

454law dg_small_n:
455  for +n: U32
456  for +hs: {U32.is_lt(n, 10) == True{} : Bool}
457  {U32.to_nat(U32.add(n, 48)) == U32.to_nat(DG(U32.to_nat(n))) : Nat}