(4steps 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 lower bound 1 1 1

1. k : 
2. f : k
3. increasing(f;k)
4. x : 
5. 0<x
6. 0x
7. x<k
8. f(0)+x-1f(x-1)
  f(0)+xf(x)


By: AllHyps (i.Unfold `increasing` i THEN InstHyp [x-1] i)


Generated subgoals:

None

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

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