Nuprl - Proof: hless eq sub less

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

all

(

a:hnum. all

(

a:hnum. (

b:hnum. implies

(

a:hnum. (

b:hnum. (le(b,a)

(

a:hnum. (

b:hnum. ,all(

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

By:	HOL "hless_eq_sub_less"

Generated subgoals:

None

About:

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