law add_div_left

bend-mathlib@0.8.1.0 · nat.bend:884

import Base

884# Adding the divisor adds one to the quotient: ((1 + b) + a) / (1 + b) = 1 + a / (1 + b).
885law add_div_left:
886  for +a: Nat
887  for +b: Nat
888  {Nat.div(Nat.add(1n+b, a), 1n+b) == 1n+Nat.div(a, 1n+b) : Nat}