Library Coq.Numbers.Integer.Abstract.ZBase
Require Export Decidable.
Require Export ZAxioms.
Require Import NZMulOrder.
Module ZBasePropFunct (
Import ZAxiomsMod :
ZAxiomsSig).
Open Local Scope IntScope.
Module Export NZMulOrderMod :=
NZMulOrderPropFunct NZOrdAxiomsMod.
Theorem Zsucc_wd :
forall n1 n2 :
Z,
n1 ==
n2 ->
S n1 ==
S n2.
Theorem Zpred_wd :
forall n1 n2 :
Z,
n1 ==
n2 ->
P n1 ==
P n2.
Theorem Zpred_succ :
forall n :
Z,
P (
S n) ==
n.
Theorem Zeq_refl :
forall n :
Z,
n ==
n.
Theorem Zeq_sym :
forall n m :
Z,
n ==
m ->
m ==
n.
Theorem Zeq_trans :
forall n m p :
Z,
n ==
m ->
m ==
p ->
n ==
p.
Theorem Zneq_sym :
forall n m :
Z,
n ~=
m ->
m ~=
n.
Theorem Zsucc_inj :
forall n1 n2 :
Z,
S n1 ==
S n2 ->
n1 ==
n2.
Theorem Zsucc_inj_wd :
forall n1 n2 :
Z,
S n1 ==
S n2 <->
n1 ==
n2.
Theorem Zsucc_inj_wd_neg :
forall n m :
Z,
S n ~=
S m <->
n ~=
m.
Theorem Zeq_dec :
forall n m :
Z,
decidable (
n ==
m).
Theorem Zeq_dne :
forall n m :
Z, ~ ~
n ==
m <->
n ==
m.
Theorem Zcentral_induction :
forall A :
Z ->
Prop,
predicate_wd Zeq A ->
forall z :
Z,
A z ->
(
forall n :
Z,
A n <->
A (
S n)) ->
forall n :
Z,
A n.
Theorem Zpred_inj :
forall n m :
Z,
P n ==
P m ->
n ==
m.
Theorem Zpred_inj_wd :
forall n1 n2 :
Z,
P n1 ==
P n2 <->
n1 ==
n2.
End ZBasePropFunct.