Nuprl - hol_arithmetic_4 LEMMAs for da

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Theorem	Name
Thm* k,n:. 0<n (r,q:. k = qn+r & r<n)	[da]
cites the following:
Thm* all Thm* (k:hnum. all Thm* (k:hnum. (n:hnum. implies Thm* (k:hnum. (n:hnum. (lt(0,n) Thm* (k:hnum. (n:hnum. ,exists Thm* (k:hnum. (n:hnum. ,(r:hnum. exists Thm* (k:hnum. (n:hnum. ,(r:hnum. (q:hnum. and Thm* (k:hnum. (n:hnum. ,(r:hnum. (q:hnum. (equal(k,add(mult(q,n),r)) Thm* (k:hnum. (n:hnum. ,(r:hnum. (q:hnum. ,lt(r,n)))))))	[hda]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html