law nat_div_mul_add

lawful-words@0.1.0.0 · LAWS.bend:563

import Base

563# (q * b + r) / b = q and (q * b + r) % b = r, for r < b.
564law nat_div_mul_add:
565  for q: Nat
566  for b: Nat
567  for r: Nat
568  for h: {Nat.is_lt(r, b) == True{} : Bool}
569  {Nat.div(Nat.add(Nat.mul(q, b), r), b) == q : Nat}