Nuprl - hol_arithmetic_2 LEMMAs for hdivision

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

Theorem	Name
Thm* all Thm* (n:hnum. implies Thm* (n:hnum. (lt(0,n) Thm* (n:hnum. ,all Thm* (n:hnum. ,(k:hnum. and Thm* (n:hnum. ,(k:hnum. (equal(k,add(mult(div(k,n),n),mod(k,n))) Thm* (n:hnum. ,(k:hnum. ,lt(mod(k,n),n)))))	[hdivision]
cites the following:
Thm* a:, n:. a = (a n)n+(a rem n)	[div_rem_sum]
Thm* a:, n:. 0(a rem n) & (a rem n)<n	[rem_bounds_1]

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