law mul_div_cancel_left

bend-mathlib@0.8.1.0 · nat.bend:2075

import Base

2075# Multiplying on the left by a positive divisor then dividing by it cancels: ((1 + b) * a) / (1 + b) = a.
2076law mul_div_cancel_left:
2077  for a: Nat
2078  for b: Nat
2079  {Nat.div(Nat.mul(1n+b, a), 1n+b) == a : Nat}