n,r:
. r<n 
(q:. ndiv(q
n+r;n) = q)Thm* (
n:hnum. all
Thm* (
n:hnum. (r:hnum. implies
Thm* (
n:hnum. (r:hnum. (lt(r,n)
Thm* (
n:hnum. (r:hnum. ,all(q:hnum. equal(div(add(mult(q,n),r),n),q)))))| Theorem | Name |
| n,r:. r<n (q:. ndiv(qn+r;n) = q) | [div_mult] |
| cites the following: | |
Thm* ( n:hnum. all
Thm* ( n:hnum. (r:hnum. implies
Thm* ( n:hnum. (r:hnum. (lt(r,n)
Thm* ( n:hnum. (r:hnum. ,all(q:hnum. equal(div(add(mult(q,n),r),n),q))))) | [hdiv_mult] |