law mod_add_div_sym

bend-mathlib@0.8.1.0 · nat.bend:4453

import Base

4453# The remainder plus the divisor times the quotient is the dividend: a % b + b * (a / b) = a, reversed to rewrite toward the simple side.
4454law mod_add_div_sym:
4455  for a: Nat
4456  for b: Nat
4457  {a == Nat.add(Nat.mod(a, b), Nat.mul(b, Nat.div(a, b))) : Nat}