Definition 2

$$0 + n = n \\ s(m) + n = s(m + n)$$

Definition 3

  add_0: 0 + ?a = ?a
add_Suc: Suc ?m + ?n = Suc (?m + ?n)

LEMMA

Zero is a left identity element of natural number addition.

$$\forall x \in \mathbb{N} : 0 + x = x$$
Proof.
LEMMA

Zero is a right identity element of natural number addition.

$$\forall x \in \mathbb{N} : x + 0 = x$$
Proof.
THEOREM

Zero is an identity element of natural number addition.

$$\forall x \in \mathbb{N} : x + 0 = 0 + x = x$$
Proof.

Zero is both a left and right identity element of natural number addition. Therefore, zero is an identity element of natural number addition.

THEOREM

$$\forall x,y \in \mathbb{N} : x + y = y + x$$
Proof.
THEOREM

$$\forall x,y,z \in \mathbb{N} : x + y + z = x + (y + z)$$
Proof.
THEOREM

$$\forall a,b,c \in \mathbb{N} : a + b = a + c \Rightarrow b = c$$
Proof 1.     ProofWiki
Proof 2.
THEOREM

$$\forall a,b,c \in \mathbb{N} : b + a = c + a \Rightarrow b = c$$
Proof 1.     ProofWiki
Proof 2.
THEOREM

Proof.

Natural number addition is both left and right-cancellative. Therefore, natural number addition is cancellative.

THEOREM

Zero is the only idempotent element of natural number addition.

\begin{align} & 0 + 0 = 0 \\ & (x + 1) + (x + 1) \ne x + 1 \end{align}
THEOREM    $$\forall x \in \mathbb{N} : x + y = x \Leftrightarrow y = 0$$
THEOREM    $$\forall a,b,c \in \mathbb{N} : a \lt b \Rightarrow c + a \lt c + b$$
Proof.
THEOREM    $$\forall a,b,c \in \mathbb{N} : a \lt b \Rightarrow a + c \lt b + c$$
Proof.
THEOREM    $$\forall a,b,c,d \in \mathbb{N} : a \lt b \wedge c \lt d \Rightarrow a + c \lt b + d$$
Proof.