Nuprl - hol_arithmetic_4 LEMMAs for mod

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

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

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