law div_mod_eq

bend-mathlib@0.8.1.0 · nat.bend:776

import Base

776# The division equation, for a positive divisor 1 + b: (a / (1 + b)) * (1 + b) + a % (1 + b) = a.
777law div_mod_eq:
778  for +a: Nat
779  for +b: Nat
780  {Nat.add(Nat.mul(Nat.div(a, 1n+b), 1n+b), Nat.mod(a, 1n+b)) == a : Nat}