law div_mod_eq_sym

bend-mathlib@0.8.1.0 · nat.bend:4065

import Base

4065# The division equation, for a positive divisor 1 + b: (a / (1 + b)) * (1 + b) + a % (1 + b) = a, reversed to rewrite toward the simple side.
4066law div_mod_eq_sym:
4067  for +a: Nat
4068  for +b: Nat
4069  {a == Nat.add(Nat.mul(Nat.div(a, 1n+b), 1n+b), Nat.mod(a, 1n+b)) : Nat}