(7steps total) PrintForm Definitions mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: increasing implies 1 2

1. k : 
2. f : k
3. i:(k-1). f(i)<f(i+1)
4. x : k
5. y : k
6. x<y
7. d:a,b:kb-a = d+1  f(a)<f(b)
  f(x)<f(y)


By: Using [`d',(y-x-1)] BackThruSomeHyp


Generated subgoals:

None

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

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