IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hless imp less add all(n:hnum. all(m:hnum. implies(lt(n,m),all(p:hnum. lt(n,add(m,p))))))
By:
HOL "hless_imp_less_add"
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html