Reading Natural Numbers in ℝ: Injectivity, Order and Pascal's Rule

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, for $n\in\mathbb{N}_{0}$ let $n_{\mathbb{R}}$ be its image in $\mathbb{R}$, and let $\binom{n}{k}$ be the binomial coefficient. Let $m,n,k\in\mathbb{N}_{0}$.

(i) Injectivity. If $m_{\mathbb{R}}=n_{\mathbb{R}}$, then $m=n$.

(ii) Order. $m\le n$ if and only if $m_{\mathbb{R}}\le n_{\mathbb{R}}$, and $m<n$ if and only if $m_{\mathbb{R}}<n_{\mathbb{R}}$.

(iii) Pascal's rule. In $\mathbb{R}$, $\binom{n}{0}=1$, $\binom{0}{k+1}=0$ and

$$\binom{n+1}{k+1}=\binom{n}{k}+\binom{n}{k+1}.$$