n,k,q:
. (
r:. k = q
n+r 
& r<n) 
ndiv(k;n) = qThm* (
n:hnum. all
Thm* (
n:hnum. (k:hnum. all
Thm* (
n:hnum. (k:hnum. (q:hnum. implies
Thm* (
n:hnum. (k:hnum. (q:hnum. (exists
Thm* (
n:hnum. (k:hnum. (q:hnum. ((r:hnum. and
Thm* (
n:hnum. (k:hnum. (q:hnum. ((r:hnum. (equal(k,add(mult(q,n),r))
Thm* (
n:hnum. (k:hnum. (q:hnum. ((r:hnum. ,lt(r,n)))
Thm* (
n:hnum. (k:hnum. (q:hnum. ,equal(div(k,n),q)))))