(10steps 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: pigeon-hole 1

1. n : 
2. m : 
3. f : nm
4. Inj(nmf)
5. p : m( List)
6. sum(||p(j)|| | j < m) = n
7. j:mx,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y]
8. j:mx:||p(j)||. (p(j))[x]<n & f((p(j))[x]) = j
  nm


By: Assert (sum(||p(j)|| | j < m)1m)


Generated subgoal:

1   sum(||p(j)|| | j < m)1m
8 steps

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

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