(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

1. k : 
2. 0<k
3. m:. (f:((k-1)m). increasing(f;k-1))  k-1m
4. m : 
5. f : km
6. increasing(f;k)
  km


By: AllHyps (InstHyp [m-1])


Generated subgoals:

1   m-1  
3 steps
2   f:((k-1)(m-1)). increasing(f;k-1)
6 steps

About:
intnatural_numbersubtractless_thanfunctionmemberimpliesallexists
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