law add_mul_div_right_sym

bend-mathlib@0.8.1.0 · nat.bend:4728

import Base

4728# Adding a multiple of a positive divisor adds to the quotient: (x + z * (1 + b)) / (1 + b) = x / (1 + b) + z, reversed to rewrite toward the simple side.
4729law add_mul_div_right_sym:
4730  for x: Nat
4731  for z: Nat
4732  for b: Nat
4733  {Nat.add(Nat.div(x, 1n+b), z) == Nat.div(Nat.add(x, Nat.mul(z, 1n+b)), 1n+b) : Nat}