law add_mul_mod_self_right

bend-mathlib@0.8.1.0 · nat.bend:3467

import Base

3467# Adding a multiple of the divisor keeps the remainder: (a + c * b) % b = a % b.
3468law add_mul_mod_self_right:
3469  for a: Nat
3470  for b: Nat
3471  for c: Nat
3472  {Nat.mod(Nat.add(a, Nat.mul(c, b)), b) == Nat.mod(a, b) : Nat}