Proposition
40
[28Z] \(≤\) is a total order relation.
Proof
Consider the proposition
\[ P(n)≐ ∀ m∈ℕ, n≤ m ∨ m≤ n \]
then \(P(0)\) is true. Let’s assume \(P(n)\); let’s fix an \(m\);
if \(m≤ n\) then \(m≤ S(n)\), by the lemma (point [2]), so \(P(Sn)\) holds;
if \(¬ m≤ n\) but \(P(n)\) holds, then \(n≤ m\) must hold, but it cannot be \(n=m\), so \(n{\lt}m\) holds: but then \(S(n)≤ m\) by the lemma (point [4]);
in any case \(P(S(n))\) is proven starting from \(P(n)\).