law dg_eq_n

lawful-fields@0.1.1.0 · proof_digits.bend:413

import Base

413law dg_eq_n:
414  for +n: U32
415  {U32.to_nat(U32.add(U32.mod(n, 10), 48)) == U32.to_nat(DG(U32.to_nat(n))) : Nat}