law mul_div_cancel_sym

bend-mathlib@0.8.1.0 · nat.bend:4417

import Base

4417# Multiplying by a positive divisor then dividing by it cancels: (a * (1 + b)) / (1 + b) = a, reversed to rewrite toward the simple side.
4418law mul_div_cancel_sym:
4419  for a: Nat
4420  for b: Nat
4421  {a == Nat.div(Nat.mul(a, 1n+b), 1n+b) : Nat}