law add_mul_mod_self_right_sym

bend-mathlib@0.8.1.0 · nat.bend:4748

import Base

4748# Adding a multiple of the divisor keeps the remainder: (a + c * b) % b = a % b, reversed to rewrite toward the simple side.
4749law add_mul_mod_self_right_sym:
4750  for a: Nat
4751  for b: Nat
4752  for c: Nat
4753  {Nat.mod(a, b) == Nat.mod(Nat.add(a, Nat.mul(c, b)), b) : Nat}