(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 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)
7. m = 0
  0-1  


By: AssertBY (f(0)  m) Auto


Generated subgoal:

1 8. f(0)  m
  0-1  

1 step

About:
intnatural_numbersubtractless_thanapplyfunction
equalmemberimpliesall
exists
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