Nuprl - Proof: less eq sub less

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: less eq sub less

a,b:

. b

(

. nnsub(a;b)<c

a<b+c)

By:	RewriteOfThm Thm* all Thm* (a:hnum. all Thm* (a:hnum. (b:hnum. implies Thm* (a:hnum. (b:hnum. (le(b,a) Thm* (a:hnum. (b:hnum. ,all(c:hnum. equal(lt(sub(a,b),c),lt(a,add(b,c))))))) (SimpsetC [`hol_to_nuprl`;`bequal`])

Generated subgoals:

None

About:

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