Nuprl - Proof: hless add 1

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

all

(

m:hnum. all

(

m:hnum. (

n:hnum. implies

(

m:hnum. (

n:hnum. (lt(n,m)

(

m:hnum. (

n:hnum. ,exists(

p:hnum. equal(m,add(n,add(p,1)))))))

By:	HOL "hless_add_1"

Generated subgoals:

None

About:

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