law add_mul_div_left

bend-mathlib@0.8.1.0 · nat.bend:3433

import Base

3433# Adding a multiple of a positive divisor adds to the quotient: (x + (1 + b) * z) / (1 + b) = x / (1 + b) + z.
3434law add_mul_div_left:
3435  for x: Nat
3436  for z: Nat
3437  for b: Nat
3438  {Nat.div(Nat.add(x, Nat.mul(1n+b, z)), 1n+b) == Nat.add(Nat.div(x, 1n+b), z) : Nat}