law mod_add_self

lawful-words@0.1.0.0 · proof_u32.bend:578

import Base

578law mod_add_self:
579  for +d: Nat
580  for +m: Nat
581  {Nat.mod(Nat.add(d, m), m) == Nat.mod(d, m) : Nat}