Nuprl - Proof: increasing le 1 2 1 1

(11steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc

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

1. k :

2. 0<k
3.

m:

. (

f:(

(k-1)

m). increasing(f;k-1))

k-1

m
4. m :

5. f :

k

m
6. increasing(f;k)
7. i :

(k-1)
8.

x,y:

k. x<y

f(x)<f(y)
9. f(0)<f(1)

f(i+1)-f(1)

(m-1)

By:	Analyze -3 THEN CaseNat 0 `i'

Generated subgoals:

1 7. i :
8. 0  i < k-1
9. x,y:k. x<y  f(x)<f(y)
10. f(0)<f(1)
11. i = 0
  f(0+1)-f(1)  (m-1)
Auto

2 7. i :
8. 0  i < k-1
9. x,y:k. x<y  f(x)<f(y)
10. f(0)<f(1)
11. i = 0
  f(i+1)-f(1)  (m-1)
1 step

About:

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

(11steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc