law quotient_remainder

stelliferous@0.0.2.0 · proofs/nat_division.bend:95

import Base

95law quotient_remainder:
96  for +q: Nat
97  for +r: Nat
98  for +b: Nat
99  for +positive: {Nat.is_lt(0n,b) == True{} : Bool}
100  for +bounded: {Nat.is_lt(r,b) == True{} : Bool}
101  {Nat.divmod(Nat.add(Nat.mul(q,b),r),b) == (q,r) : Nat & Nat}