Library Coq.Numbers.NatInt.NZAdd
Require Import NZAxioms.
Require Import NZBase.
Module NZAddPropFunct (
Import NZAxiomsMod :
NZAxiomsSig).
Module Export NZBasePropMod :=
NZBasePropFunct NZAxiomsMod.
Open Local Scope NatIntScope.
Theorem NZadd_0_r :
forall n :
NZ,
n + 0 ==
n.
Theorem NZadd_succ_r :
forall n m :
NZ,
n +
S m ==
S (
n +
m).
Theorem NZadd_comm :
forall n m :
NZ,
n +
m ==
m +
n.
Theorem NZadd_1_l :
forall n :
NZ, 1 +
n ==
S n.
Theorem NZadd_1_r :
forall n :
NZ,
n + 1 ==
S n.
Theorem NZadd_assoc :
forall n m p :
NZ,
n + (
m +
p) == (
n +
m) +
p.
Theorem NZadd_shuffle1 :
forall n m p q :
NZ, (
n +
m) + (
p +
q) == (
n +
p) + (
m +
q).
Theorem NZadd_shuffle2 :
forall n m p q :
NZ, (
n +
m) + (
p +
q) == (
n +
q) + (
m +
p).
Theorem NZadd_cancel_l :
forall n m p :
NZ,
p +
n ==
p +
m <->
n ==
m.
Theorem NZadd_cancel_r :
forall n m p :
NZ,
n +
p ==
m +
p <->
n ==
m.
Theorem NZsub_1_r :
forall n :
NZ,
n - 1 ==
P n.
End NZAddPropFunct.