law mod_add_mul

lawful-words@0.1.0.0 · proof_nat.bend:1175

import Base

1175# Adding a multiple of x does not change the remainder by x.
1176law mod_add_mul:
1177  for +j: Nat
1178  for +x: Nat
1179  for +z: Nat
1180  {Nat.mod(Nat.add(Nat.mul(j, x), z), x) == Nat.mod(z, x) : Nat}