Natural Numbers and Factorials Read in the Reals: the Order Carries Over, One Is Least, and Factorials Are Positive, Recursive and Nondecreasing

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, an element $n$ of $\mathbb{N}_{0}$ read in $\mathbb{R}$ denotes its image $n_{\mathbb{R}}$, as in Commutative Rings, Fields and Ordered Fields: Standard Notation (iv), and $n!$ is the factorial of $n\in\mathbb{N}_{0}$.

(i) For all $m,n\in\mathbb{N}_{0}$ with $m\le n$ in $\mathbb{N}_{0}$, $m\le n$ in $\mathbb{R}$.

(ii) For every $n\in\mathbb{N}$, $1\le n$ in $\mathbb{R}$.

(iii) For every $k\in\mathbb{N}_{0}$, in $\mathbb{R}$: $1\le k!$, so that $0<k!$ and $k!\neq0$; $(k+1)!=(k+1)\cdot k!$; and $k!\le(k+1)!$.