Nuprl - Proof: increasing le 1 2 2

(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 2

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)

increasing(

i.f(i+1)-f(1);k-1)

By:	All (Unfold `increasing`) THEN Reduce 0 THEN InstHyp [i+1] -2

Generated subgoals:

None

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