Nuprl - mb_nat LEMMAs for disjoint_increasing

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

Rank	Theorem	Name
2	Thm* m,n,k:, f:(nm), g:(km). Thm* increasing(f;n) Thm* Thm* increasing(g;k) Thm* Thm* (i:m. (j:n. i = f(j)) (j:k. i = g(j))) Thm* Thm* (j1:n, j2:k. f(j1) = g(j2)) m = n+k	[disjoint_increasing_onto]
cites the following:
1	Thm* k,m:. (f:(km). Inj(k; m; f)) km	[injection_le]
1	Thm* k,m:, f:(km). increasing(f;k) Inj(k; m; f)	[increasing_inj]

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