Natural number addition


Definition 1

ProofWiki

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   

Natural number addition is commutative.

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

Natural number addition is associative.

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

Natural number addition is left-cancellative.

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

Natural number addition is right-cancellative.

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

Natural number addition is cancellative.

Proof.    

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

Proper supersets