Nuprl - mb_nat LEMMAs for pigeon_DASH

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

Rank	Theorem	Name
4	Thm* n,m:, f:(nm). Inj(n; m; f) nm	[pigeon-hole]
cites the following:
3	Thm* n,k:, c:(nk). Thm* p:(k( List)). Thm* sum(\|\|p(j)\|\| \| j < k) = n Thm* & (j:k, x,y:\|\|p(j)\|\|. x<y (p(j))[x]>(p(j))[y]) Thm* & (j:k, x:\|\|p(j)\|\|. (p(j))[x]<n & c((p(j))[x]) = j)	[finite-partition]
0	Thm* k,b:, f:(k). (x:k. f(x)b) sum(f(x) \| x < k)bk	[sum_bound]

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