Library Coq.Numbers.Natural.Abstract.NAdd
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.
Theorem eq_add_succ :
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).
Theorem add_dichotomy :
forall n m :
N, (
exists p :
N,
p +
n ==
m) \/ (
exists p :
N,
p +
m ==
n).
End NAddPropFunct.