Constructive proof of pigeonhole principle I'm trying to prove Pigeonhole principle with Coq proof assistant.
Here is how I defined it:
Theorem pigeonhole
    :  forall m n : nat, m < n
    -> forall f : nat -> nat, (forall i, f i < m)
    -> exists i, i < n
    -> exists j, j < i /\ f i = f j.

After spending some time on attempts to prove it by induction I found this discussion (https://math.stackexchange.com/a/228604/15013) that suggest it is impossible.
Is it possible (and how) to prove Pigeonhole principle without using contradiction?
Using principle of explosion is fine, but excluded middle is not accepted.
 A: Here is a proof that would go through in Bishop's system and similar systems where equality of natural numbers is decidable. 
We only need to prove the case $n = m+ 1$, because this implies the general case $n > m$. So we will work with functions from $n = \{0, 1, \ldots, n-1\}$ to $m = n - 1 = \{0, \ldots, m-1\}$. 
The proof will be by induction on $n$. The case $n = 1$ is impossible (there is no function from $1$ to $0$) so the base case is $n = 2$. In this case $f(0) = f(1) = 0$ so we're done.
For the inductive case, assume $f$ is a function from $n = m+1$ to $m$ where $m > 1$. We don't have full excluded middle constructively, but we do have constructively that either there is some $i < m$ with $f(i) = f(m)$, or there is not. Speaking formally, we can prove $$(\forall f)(\forall k)(\forall m)[(\exists i < m)[f(i) = k] \lor \lnot (\exists i < m)[f(i) = k]]$$ by induction on $m$, with $f$ and $k$ as parameters.
So, working constructively, we can split into those two cases: either there is some $i < m$ with $f(i) = f(m)$, or there is not. In the first case, we are done already.
In the second case, we make a new function $g$ from $m$ to $m - 1$ so that $g(a) = f(a)$ whenever $f(a) < f(m)$, and $g(a) = f(a) -1$ when $f(a) > f(m)$. This is a sound definition because we have assumed $f(a) \not = f(m)$ for all $a < m$. Now we can apply the inductive hypothesis to $g$ to find $i,j < m$ with $g(i) = g(j)$; then $f(i) = f(j)$ also and we are done. 

Here is a guide to prove $$(\forall f)(\forall k)(\forall m)[(\exists i < m)[f(i) = k] \lor \lnot (\exists i < m)[f(i) = k]]$$
The first step is to prove $(\forall x)(\forall y)[x = y \lor x \not = y]$. This is proved by induction on $x$ with $y$ as a parameter.


*

*For the base case, we prove $(\forall y)[y = 0 \lor y \not = 0]$ from the axioms 
1) $0 \not = S(z)$
2) $ y = 0 \lor ( \exists z)[y = S(z)]$.

*For the inductive case, we use the additional axiom $x = y  \leftrightarrow S(x) = S(y)$. 
Once we have the first step, then we can prove the desired formula by induction on $m$ with $k$ and $f$ as parameters. 


*

*The base case is $\lnot (\exists i < 0)[f(i) = k]$. 

*For the inductive case, we use the additional axiom $x = S(y) \to z < x \to z < y \lor z = y$ (or we derive this separately). 
