IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
increasing lower bound111 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:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html