law div_add_mod

bend-mathlib@0.8.1.0 · nat.bend:3523

import Base

3523# The divisor times the quotient plus the remainder is the dividend: b * (a / b) + a % b = a.
3524law div_add_mod:
3525  for a: Nat
3526  for b: Nat
3527  {Nat.add(Nat.mul(b, Nat.div(a, b)), Nat.mod(a, b)) == a : Nat}