EDB — 1YP

[1YP] Show that every $n\in \mathbb{N}$ with $n\ne 0$ is successor of another $k\in \mathbb{N}$, proving by induction on $n$ this proposition

This shows that the successor function

is bijective.

If $n\ne 0$, we will call $S^{-1}(n)$ the predecessor of $n$.

(Part of this result applies more generally, see [1Z1]↺↻)