law dgv

lawful-fields@0.1.1.0 · proof_digits.bend:395

import Base

395law dgv:
396  for +x: Nat
397  {U32.to_nat(DG(x)) == Nat.add(48n, Nat.mod(x, 10n)) : Nat}