hol arithmetic 5 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
TheoremName
Thm* m,n,x:. nnsub(m;n)<x  m<n+x & 0<x[sub_right_less]
cites the following:
Thm* all
Thm* (m:hnum. all
Thm* (m:hnum. (n:hnum. all
Thm* (m:hnum. (n:hnum. (p:hnum. equal
Thm* (m:hnum. (n:hnum. (p:hnum. (lt(sub(m,n),p)
Thm* (m:hnum. (n:hnum. (p:hnum. ,and(lt(m,add(n,p)),lt(0,p))))))		[hsub_right_less]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol arithmetic 5 Sections HOLlib Doc