Nuprl - Proof: increasing implies 1

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

1. k :

2. f :

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

k
5. y :

k
6. x<y

f(x)<f(y)

By:	Assert (d:, a,b:k. b-a = d+1 f(a)<f(b))

Generated subgoals:

1   d:, a,b:k. b-a = d+1  f(a)<f(b)
4 steps

2 7. d:, a,b:k. b-a = d+1  f(a)<f(b)
  f(x)<f(y)
1 step

About:

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

1	d:, a,b:k. b-a = d+1 f(a)<f(b)	4 steps
2	7. d:, a,b:k. b-a = d+1 f(a)<f(b) f(x)<f(y)	1 step