Nuprl - hol_arithmetic_4 LEMMAs for less_eq_less_eq

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

Theorem	Name
Thm* m,n,x,q:. mx & nq m+nx+q	[less_eq_less_eq_mono]
cites the following:
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. (q:hnum. implies Thm* (m:hnum. (n:hnum. (p:hnum. (q:hnum. (and(le(m,p),le(n,q)) Thm* (m:hnum. (n:hnum. (p:hnum. (q:hnum. ,le(add(m,n),add(p,q)))))))	[hless_eq_less_eq_mono]

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