Library Coq.Numbers.Natural.Abstract.NAdd


Require Export NBase.

Module NAddProp (Import N : NAxiomsMiniSig´).
Include NBaseProp N.

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.