Library Coq.Numbers.Natural.Abstract.NAdd
For theorems about add that are both valid for N and Z, see NZAdd Now comes theorems valid for natural numbers but not for Z
Theorem eq_add_0 : forall n m, n + m == 0 <-> n == 0 /\ m == 0.
Theorem eq_add_succ :
forall n m, (exists p, n + m == S p) <->
(exists n', n == S n') \/ (exists m', m == S m').
Theorem eq_add_1 : forall n m,
n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1.
Theorem succ_add_discr : forall n m, m ~= S (n + m).
Theorem add_pred_l : forall n m, n ~= 0 -> P n + m == P (n + m).
Theorem add_pred_r : forall n m, m ~= 0 -> n + P m == P (n + m).
End NAddProp.