law n_div_mul_add

lawful-arrays@0.1.0.0 · proof_words.bend:80

import Base

80law n_div_mul_add:
81  for +q: Nat
82  for +b: Nat
83  for +r: Nat
84  for +h: {Nat.is_lt(r, b) == True{} : Bool}
85  {Nat.div(Nat.add(Nat.mul(q, b), r), b) == q : Nat}