Require Export NBase.

Module NAddPropFunct (Import NAxiomsMod : NAxiomsSig).
Module Export NBasePropMod := NBasePropFunct NAxiomsMod.

Open Local Scope NatScope.

forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 + m1 == n2 + m2.
Theorem add_0_l : forall n : N, 0 + n == n.
Theorem add_succ_l : forall n m : N, (S n) + m == S (n + m).
Theorems that are valid for both natural numbers and integers
Theorem add_0_r : forall n : N, n + 0 == n.
Theorem add_succ_r : forall n m : N, n + S m == S (n + m).
Theorem add_comm : forall n m : N, n + m == m + n.
Theorem add_assoc : forall n m p : N, n + (m + p) == (n + m) + p.
Theorem add_shuffle1 : forall n m p q : N, (n + m) + (p + q) == (n + p) + (m + q).
Theorem add_shuffle2 : forall n m p q : N, (n + m) + (p + q) == (n + q) + (m + p).
Theorem add_1_l : forall n : N, 1 + n == S n.
Theorem add_1_r : forall n : N, n + 1 == S n.
Theorem add_cancel_l : forall n m p : N, p + n == p + m <-> n == m.
Theorem add_cancel_r : forall n m p : N, n + p == m + p <-> n == m.
Theorem eq_add_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0.

forall n m : N, (exists p : N, n + m == S p) <->
(exists n' : N, n == S n') \/ (exists m' : N, m == S m').

Theorem eq_add_1 : forall n m : N,
n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1.

Theorem succ_add_discr : forall n m : N, m ~= S (n + m).

Theorem add_pred_l : forall n m : N, n ~= 0 -> P n + m == P (n + m).

Theorem add_pred_r : forall n m : N, m ~= 0 -> n + P m == P (n + m).