law add_mul_div_right

bend-mathlib@0.8.1.0 · nat.bend:3411

import Base

3411# Adding a multiple of a positive divisor adds to the quotient: (x + z * (1 + b)) / (1 + b) = x / (1 + b) + z.
3412law add_mul_div_right:
3413  for x: Nat
3414  for z: Nat
3415  for b: Nat
3416  {Nat.div(Nat.add(x, Nat.mul(z, 1n+b)), 1n+b) == Nat.add(Nat.div(x, 1n+b), z) : Nat}