law add_mod_left_sym

bend-mathlib@0.8.1.0 · nat.bend:4408

import Base

4408# Adding the divisor does not change the remainder: (b + a) % b = a % b, reversed to rewrite toward the simple side.
4409law add_mod_left_sym:
4410  for a: Nat
4411  for b: Nat
4412  {Nat.mod(a, b) == Nat.mod(Nat.add(b, a), b) : Nat}