hol arithmetic 4 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
TheoremName
Thm* n,m:m<n  0<nnsub(n;m)[sub_less_0]
cites the following:
Thm* all(n:hnum. all(m:hnum. equal(lt(m,n),lt(0,sub(n,m)))))[hsub_less_0]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol arithmetic 4 Sections HOLlib Doc