Nuprl - Proof: increasing implies 1 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: increasing implies 1 1 2

1. k :

2. f :

(k-1). f(i)<f(i+1)
4. x :

k
5. y :

k
6. x<y
7. d :

8. 0<d
9.

a,b:

k. b-a = d-1+1

f(a)<f(b)

a,b:

k. b-a = d+1

f(a)<f(b)

By:	Auto THEN InstHyp [a+1;b] -4

Generated subgoal:

1 10. a : k
11. b : k
12. b-a = d+1
13. f(a+1)<f(b)
f(a)<f(b)
1 step

About:

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