law add_div_left_sym

bend-mathlib@0.8.1.0 · nat.bend:4074

import Base

4074# Adding the divisor adds one to the quotient: ((1 + b) + a) / (1 + b) = 1 + a / (1 + b), reversed to rewrite toward the simple side.
4075law add_div_left_sym:
4076  for +a: Nat
4077  for +b: Nat
4078  {1n+Nat.div(a, 1n+b) == Nat.div(Nat.add(1n+b, a), 1n+b) : Nat}