law mul_div_cancel

bend-mathlib@0.8.1.0 · nat.bend:2059

import Base

2059# Multiplying by a positive divisor then dividing by it cancels: (a * (1 + b)) / (1 + b) = a.
2060law mul_div_cancel:
2061  for a: Nat
2062  for b: Nat
2063  {Nat.div(Nat.mul(a, 1n+b), 1n+b) == a : Nat}