The Pigeonhole Principle, injective version

We need to prove that the number of elements of a finite set is unambiguous.
We prove the Pigeonhole Principle:

• (J)
  For $n$ and $m$ positive integers, let $f: \mathbb{N}_m \rightarrow \mathbb{N}_n$ be an injection.
  Then $m \le n$.
• (K) Also if $m = n$, then $f$ is a bijection.

Proof:
For (J), assume that the proposition is false.
So for some integers $m$ and $n$ with $m > n\ge 1$, we have an injection $f: \mathbb{N}_m \rightarrow \mathbb{N}_n$.
We want to reach a contradiction.
First we observe that $n > 1$ since if $f: \mathbb{N}_m \rightarrow \mathbb{N}_1$ is a map and $m \ge 2$, then, since $\mathbb{N}_1 = \{1\}$, we have $1 \in \mathbb{N}_m$ and $2\in \mathbb{N}_m$, so $f(1) = f(2) = 1$, yet $1 \ne 2$, so $f$ cannot be injective.
Now take $n > 1$ to be the smallest positive integer, so that the proposition is false; this exists by POW.
Let $f(m) = k \in \mathbb{N}_n$.
Using the (injective) switching map $S_{k, n}: \mathbb{N}_n \rightarrow \mathbb{N}_n$, define $g = S_{k, n} \circ f$.
Then $g$ is a well-defined map from $\mathbb{N}_m$ to $\mathbb{N}_n$ and is a composition of injections, so is injective.
Also we have $g(m) = S_{k,n}(f(m)) = S_{k, n}(k) = n$.
Since $g$ is injective, if $t$ is an integer, such that $1 \le t< m$, we have $g(t) \ne g(m)$ so $g(t) \ne n$, so $1\le g(t) \le n-1$.
Now define $h: \mathbb{N}_{m - 1} \rightarrow \mathbb{N}_{n -1}$ by the formula: $h(t) = g(t)$, for each $t \in \mathbb{N}_{m-1}$.
Then since $g(t) < n$, for any $t \in \mathbb{N}_{m-1}$ the map $h$ is well-defined.
Also if $h(s) = h(t)$, for $s$ and $t$ in $\mathbb{N}_{m - 1}$, we have $g(s) = g(t)$, so $s = t$.
So $h$ is an injection from $\mathbb{N}_{m - 1}\rightarrow \mathbb{N}_{n-1}$ and $m - 1> n - 1$.
This is contrary to the definition of $n$, so theorem (J) is proved.

For (K), for some $n \in\mathbb{N}$ let an injection $f: \mathbb{N}_n \rightarrow \mathbb{N}_n$ be given, which is not a bijection.
By theorem (A), proved above, if $f$ is not a bijection, then $n > 1$ and there is an injection $g: \mathbb{N}_n \rightarrow \mathbb{N}_{n - 1}$.
But this contradicts theorem (J), just proved above.
So $f$ is a bijection and we are done.