law div_add_mod_sym

bend-mathlib@0.8.1.0 · nat.bend:4776

import Base

4776# The divisor times the quotient plus the remainder is the dividend: b * (a / b) + a % b = a, reversed to rewrite toward the simple side.
4777law div_add_mod_sym:
4778  for a: Nat
4779  for b: Nat
4780  {a == Nat.add(Nat.mul(b, Nat.div(a, b)), Nat.mod(a, b)) : Nat}