mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
4Thm* n,m:f:(nm). Inj(nmf nm[pigeon-hole]
cites the following:
3Thm* n,k:c:(nk).
Thm* p:(k( List)). 
Thm* sum(||p(j)|| | j < k) = n
Thm* & (j:kx,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y])
Thm* & (j:kx:||p(j)||. (p(j))[x]<n & c((p(j))[x]) = j)
[finite-partition]
0Thm* k,b:f:(k). (x:kf(x)b sum(f(x) | x < k)bk[sum_bound]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb nat Sections MarkB generic Doc