Prove Proposition 2.2.12.
Proposition 2.2.12 (basic properties of order for natural numbers):
Let $a, b, c$ be natural numbers. Then
(a) (Order is reflexive) $a\ge a$.
(b) (Order is transitive) If $a\ge b$ and $b\ge c$, then $a\ge c$.
(c) (Order is antisymmetric) If $a\ge b$ and $b\ge a$, then $a=b$.
(d) (Addition preserves order) $a\ge b$ if and only if $a+c\ge b+c$.
(e) $a<b$ if and only if $a++\le b$.
(f ) $a<b$ if and only if $b=a+d$ for some positive number $d$.
(a) By Definition 2.2.11 (ordering of the natural numbers) we have $a\ge a$ if and only if $a=a+x$ for some natural number $x$.
To show $a\ge a$, it is sufficient to show $a=a+x$ is true for some natural number $x$. Choosing $x=0$ gives $a=a+0$. By the symmetry axiom of equality this is $a+0=a$, which is indeed true by Lemma 2.2.2.
We have shown $a=a+x$ is true for some natural number $x$, and so by Definition 2.2.11 we conclude $a\ge a$.
(b) By Definition 2.2.11 (ordering of the natural numbers) we have $a\ge b$ if and only if $a=b+x$ for some natural number $x$, and $b\ge c$ if and only if $b=c+y$ for some natural number $y$.
Together we have $a=(c+y)+x$ for some natural numbers $x,y$. By Proposition 2.2.5 (addition is associative), we have $a=c+(y+x)$. The sum of two natural numbers, $x$ and $y$, is also a natural number $x+y$. By Definition 2.2.11 this means $a\ge c$.
For completeness we should prove the sum of two natural numbers is a natural number. We'll use induction. Let $P(a)$ be the statement that the sum $a+b$ of natural numbers $a$ and $b$ is also a natural number. We need to show the base case $P(0)$, and the inductive step $P(a)\implies P(a++)$. The base case $P(0)$ states $0+b$ is a natural number. Definition 2.2.1 (addition of natural numbers) tells us $0+b:=b$ where $b$ is a natural number, and so the base case is true. For the inductive step we need to show $P(a++)$, assuming $P(a)$. That is, we want to show $(a++)+b$ is a natural number. Again by Definition 2.2.1, we have $(a++)+b:=(a+b)++$. The assumption $P(a)$ tells us $(a+b)$ is a natural number, and Axiom 2.2 tells us $(a+b)++$ is a natural number, proving the inductive step. So by induction we have shown the sum of two natural numbers is a natural number.
(c) By Definition 2.2.11 (ordering of the natural numbers) we have $a\ge b$ if and only if $a=b+x$ for some natural number $x$. By the same definition we have $b\ge a$ if and only if $b=a+y$ for some natural number $y$.
Together this means $a=(a+y)+x$ for some natural numbers $x,y$. By Proposition 2.2.5 (addition is associative), we have $a=a+(y+x)$. Intuitively we can see $x$ and $y$ must both be zero. Let's show this.
By Proposition 2.2.6 (cancellation law) this gives $0=y+x$. The symmetry axiom of equality gives us $y+x=0$. Corollary 2.2.9 tells us that both $x=0$ and $y=0$.
Substituting $x=0$ into $a=b+x$ gives us $a=b+0$. Lemma 2.2.2 tells us $b+0=b$ which finally gives us $a=b$.
(d) We need to show both $a\ge b\implies a+c\ge b+c$ and $a\ge b\impliedby a+c\ge b+c$.
$(\implies)$
By Definition 2.2.11 (ordering of the natural numbers) we have $a\ge b\implies a=b+x$ for some natural number $x$.
By the substitution axiom of equality, $a=b+x$ means $a+c=(b+x)+c$, for some natural number $c$. By Proposition 2.2.5 (addition is associative) we have $a+c=b+(x+c)$. Proposition 2.2.4 (addition is commutative) gives us $a+c=b+(c+x)$. Applying Proposition 2.2.5 again gives us $a+c=(b+c)+x$. By Definition 2.2.11 this means $a+c\ge b+c$, and so we have shown $a\ge b\implies a+c\ge b+c$.
$(\impliedby)$
By Definition 2.2.11 (ordering of the natural numbers) we have $a+c\ge b+c\implies a+c=(b+c)+y$ for some natural number $y$. Proposition 2.2.4 (addition is commutative) we have $c+a=(c+b)+y$. Proposition 2.2.5 (addition is associative) then gives us $c+a=c+(b+y)$. The Proposition 2.2.6 (cancellation law) reduces this to $a=b+y$, which by Definition 2.2.11 means $a\ge b$, and so we have shown $a+c\ge b+c\implies a\ge b$.
By showing both $a\ge b\implies a+c\ge b+c$ and $a+c\ge b+c\implies a\ge b$, we have shown $a\ge b\iff a+c\ge b+c$.
(e) We need to show both $a<b\implies a++\le b$ and $a<b\impliedby a++\le b$.
$(\implies)$
By Definition 2.2.11 (ordering of the natural numbers) $a<b$ implies both $b=a+x$ for some natural number $x$, and $b\ne a$.
For the purpose of contradiction let's assume $x=0$. This would mean $b=a+0$, which by Lemma 2.2.2 gives $b=a$. This contradicts $b\ne a$. And so $x\ne0$, that is, $x$ is a positive number.
By Lemma 2.2.10 there exists a unique natural number $y$ such that $y++=x$. This gives us $b=a+(y++)$. By Lemma 2.2.3 this is $b=(a+y)++$, and by Definition 2.2.1 (addition of natural numbers) this is $b=(a++)+y$. By Definition 2.2.11 this means $a++\le b$, and so we have shown $a<b\implies a++\le b$.
$(\impliedby)$
By Definition 2.2.11 (ordering of the natural numbers) $a++\le b$ implies $b=(a++)+x$ for some natural number $x$.
Definition 2.2.1 gives us $b=(a+x)++$, and by Lemma 2.2.3 this is $b=a+(x++)$.
For the purpose of contradiction let's assume $a=b$. This would mean $b=b+(x++)$, and by Definition 2.2.1 this is $0+b=b+(x++)$. The symmetry axiom of equality gives us $b+0=b+(x++)$. Proposition 2.2.6 (cancellation law) then gives us $0=x++$. This contradicts Axiom 2.3, and so $a\ne b$.
By Definition 2.2.11, having both $b=a+(x++)$ and $a\ne b$ means $a<b$, and so we have shown $a++\le b\implies a<c$.
By showing both $a<b\implies a++\le b$ and $a++\le b\implies a<c$, we have shown $a<b\iff a++\le b$.
(f) We need to show both $a<b\implies b=a+d$ and $a<b\impliedby b=a+d$, where $d$ is a positive number.
$(\implies)$
By Definition 2.2.11 (ordering of the natural numbers) $a<b$ implies both $b=a+d$ for some natural number $d$, and $b\ne a$.
For the purpose of contradiction let's assume $d=0$. This would mean $b=a+0$, which by Lemma 2.2.2 gives $b=a$. This contradicts $b\ne a$. And so $d\ne0$, that is, $d$ is a positive number.
We have shown that $a<b\implies b=a+d$, where $d$ is a positive number.
$(\impliedby)$
For the purpose of contradiction let's assume $b=a$. This would mean $a=a+d$, which by Definition 2.2.1 (addition of natural numbers) is gives $0+a=a+d$. By the symmetry axiom of equality, this is $a+0=a+d$. Applying Proposition 2.2.6 (cancellation law) then gives $0=d$, which is $d=0$ by the symmetry axiom of equality. This contradicts $d$ being a positive number. And so $b\ne a$.
Applying Definition 2.2.1 to $b=a+d$ and $b\ne a$ gives us $a<b$, and so we have shown $b=a+d\implies a<c$, where $d$ is a positive number.
By showing both $a<b\implies b=a+d$ and $b=a+d\implies a<c$, where $d$ is a positive number, we have shown $a<b\iff b=a+d$.
