Nuprl - Proof: hless eq add sub

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

all

(

c:hnum. all

(

c:hnum. (

b:hnum. implies

(

c:hnum. (

b:hnum. (le(c,b)

(

c:hnum. (

b:hnum. ,all(

a:hnum. equal(sub(add(a,b),c),add(a,sub(b,c)))))))

By:	HOL "hless_eq_add_sub"

Generated subgoals:

None

About:

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