law nat_div_mod

lawful-words@0.1.0.0 · LAWS.bend:491

import Base

491# a = (a / b) * b + a % b (also for b = 0: a / 0 = 0 and a % 0 = a).
492law nat_div_mod:
493  for a: Nat
494  for b: Nat
495  {Nat.add(Nat.mul(Nat.div(a, b), b), Nat.mod(a, b)) == a : Nat}