law div_mod

lawful-words@0.1.0.0 · proof_nat.bend:1007

import Base

1007# a = (a / b) * b + a % b.
1008law div_mod:
1009  for +a: Nat
1010  for +b: Nat
1011  {Nat.add(Nat.mul(Nat.div(a, b), b), Nat.mod(a, b)) == a : Nat}