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

### Proof of a lemma for the Pigeon-hole principle

Show Thm* m: f:( m   ). Inj( m f  ( x: my: xf(x) = f(y)).

That is, given a non-injective assigment of integers to a finite collection we can find two objects (with the second objects y preceding the first value x) that are assigned the same value.
This reduces to showing the contrapositive, namely ( x: my: xf(x) = f(y))  Inj( m f)

(computationally, since there are only finitely many choices for x and y in the specified domain, one could just exhaustively try them all and see if there is a pair whose assignments by f agree).
So assuming that

 (1) ( x: m, y: x. f(x) = f(y))

and employing the definition

Def  Inj(ABf) == a1,a2:Af(a1) = f(a2 B  a1 = a2

our proof reduces to showing that if

 (2) f(a1) = f(a2)

then a1 = a2. This further reduces to showing that a1<a2 & a2<a1

which each follow from assumptions (1) and (2).

QED

This is a lemma for a proof of the pigeon-hole principle

Thm* m,k: f:( m   k). k<m  ( x,y: mx y & f(x) = f(y))