law add_mod_left

bend-mathlib@0.8.1.0 · nat.bend:2043

import Base

2043# Adding the divisor does not change the remainder: (b + a) % b = a % b.
2044law add_mod_left:
2045  for a: Nat
2046  for b: Nat
2047  {Nat.mod(Nat.add(b, a), b) == Nat.mod(a, b) : Nat}