law add_mul_div_left_sym

bend-mathlib@0.8.1.0 · nat.bend:4738

import Base

4738# Adding a multiple of a positive divisor adds to the quotient: (x + (1 + b) * z) / (1 + b) = x / (1 + b) + z, reversed to rewrite toward the simple side.
4739law add_mul_div_left_sym:
4740  for x: Nat
4741  for z: Nat
4742  for b: Nat
4743  {Nat.add(Nat.div(x, 1n+b), z) == Nat.div(Nat.add(x, Nat.mul(1n+b, z)), 1n+b) : Nat}