Nuprl - Proof: less eq add sub

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

c,b:

. c

(

. nnsub(a+b;c) = a+nnsub(b;c))

By:	RewriteOfThm Thm* all Thm* (c:hnum. all Thm* (c:hnum. (b:hnum. implies Thm* (c:hnum. (b:hnum. (le(c,b) Thm* (c:hnum. (b:hnum. ,all Thm* (c:hnum. (b:hnum. ,(a:hnum. equal(sub(add(a,b),c),add(a,sub(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