Nuprl - Proof: increasing implies 1 1

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

1. k :

2. f :

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

k
5. y :

k
6. x<y

, a,b:

k. b-a = d+1

f(a)<f(b)

By:	Analyze 0 THEN NatInd -1

Generated subgoals:

1   a,b:k. b-a = 0+1  f(a)<f(b)
1 step

2 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)
2 steps

About:

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

1	a,b:k. b-a = 0+1 f(a)<f(b)	1 step
2	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)	2 steps