law div_mul_add

lawful-words@0.1.0.0 · proof_nat.bend:1072

import Base

1072law div_mul_add:
1073  for +q: Nat
1074  for +b: Nat
1075  for +r: Nat
1076  for +h: {Nat.is_lt(r, b) == True{} : Bool}
1077  {Nat.div(Nat.add(Nat.mul(q, b), r), b) == q : Nat}