(22steps 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: disjoint increasing onto 1

1. m : 
2. n : 
3. k : 
4. f : nm
5. g : km
6. increasing(f;n)
7. increasing(g;k)
8. i:m. (j:ni = f(j))  (j:ki = g(j))
9. j1:nj2:kf(j1) = g(j2)
  m = n+k  


By: Assert (mn+k)


Generated subgoals:

1   mn+k
11 steps
2 10. mn+k
  m = n+k  

9 steps

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

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