law mul_div_cancel_left_sym

bend-mathlib@0.8.1.0 · nat.bend:4426

import Base

4426# Multiplying on the left by a positive divisor then dividing by it cancels: ((1 + b) * a) / (1 + b) = a, reversed to rewrite toward the simple side.
4427law mul_div_cancel_left_sym:
4428  for a: Nat
4429  for b: Nat
4430  {a == Nat.div(Nat.mul(1n+b, a), 1n+b) : Nat}