恕我吐槽一句，$n+!+$ 不丑吗…… $n’$ 不香吗……
我真傻，真的。我单知道洛谷题解里有在公式里出现的 ++，我不知道陶哲轩实分析也有。
下文用 $n’$ 代替 $n+!+$。
2.1 Peano 公理
2.2 加法
2.2.1
对 $c$ 使用归纳法。
$P(c)$：$\forall a,b:(a+b)+c=a+(b+c)$；
$P(0)$：显然；
$P(c)\Rightarrow P(c’)$：$(a+b)+c’=[(a+b)+c]’=[a+(b+c)]’=a+(b+c)’=a+(b+c’)$。
$\square$
2.2.2
存在性：
使用归纳法证明 $P(a)=\forall a:\exist b:b’=a+1$。
$P(0)$：$b=0$ 即可。
$P(a)\Rightarrow P(a’)$：$(b’)’=b’+1=(a+1)+1=a’+1$。
唯一性：
由 Peano 公理立即得到。
$\square$
2.2.3
(a)
$\forall a:a=0+a$.
$\square$
(b)
由于 $\exist m:a=m+b$，$\exist n:b=n+c$，所以 $a=m+b=m+(n+c)=(m+n)+c$。
$\square$
(c)
由于 $\exist m:a=m+b$，$\exist n:b=n+a$，所以 $a=m+b=m+(n+a)=(m+n)+a$。使用消去律立即得到。
$\square$
(d)
$a\ge b\Rightarrow a+c\ge b+c$：