## 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)

THEOREM

Zero is a left identity element of natural number addition.

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

Zero is a right identity element of natural number addition.

$$\forall x \in \mathbb{N} : x + 0 = x$$
Proof.
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$$