Library Coq.Numbers.Integer.Binary.ZBinary
Require Import ZMulOrder.
Require Import ZArith.
Open Local Scope Z_scope.
Module ZBinAxiomsMod <:
ZAxiomsSig.
Module Export NZOrdAxiomsMod <:
NZOrdAxiomsSig.
Module Export NZAxiomsMod <:
NZAxiomsSig.
Definition NZ :=
Z.
Definition NZeq := (@
eq Z).
Definition NZ0 := 0.
Definition NZsucc :=
Zsucc'.
Definition NZpred :=
Zpred'.
Definition NZadd :=
Zplus.
Definition NZsub :=
Zminus.
Definition NZmul :=
Zmult.
Theorem NZeq_equiv :
equiv Z NZeq.
Add Relation Z NZeq
reflexivity proved by (
proj1 NZeq_equiv)
symmetry proved by (
proj2 (
proj2 NZeq_equiv))
transitivity proved by (
proj1 (
proj2 NZeq_equiv))
as NZeq_rel.
Add Morphism NZsucc with signature NZeq ==>
NZeq as NZsucc_wd.
Add Morphism NZpred with signature NZeq ==>
NZeq as NZpred_wd.
Add Morphism NZadd with signature NZeq ==>
NZeq ==>
NZeq as NZadd_wd.
Add Morphism NZsub with signature NZeq ==>
NZeq ==>
NZeq as NZsub_wd.
Add Morphism NZmul with signature NZeq ==>
NZeq ==>
NZeq as NZmul_wd.
Theorem NZpred_succ :
forall n :
Z,
NZpred (
NZsucc n) =
n.
Theorem NZinduction :
forall A :
Z ->
Prop,
predicate_wd NZeq A ->
A 0 -> (
forall n :
Z,
A n <->
A (
NZsucc n)) ->
forall n :
Z,
A n.
Theorem NZadd_0_l :
forall n :
Z, 0 +
n =
n.
Theorem NZadd_succ_l :
forall n m :
Z, (
NZsucc n) +
m =
NZsucc (
n +
m).
Theorem NZsub_0_r :
forall n :
Z,
n - 0 =
n.
Theorem NZsub_succ_r :
forall n m :
Z,
n - (
NZsucc m) =
NZpred (
n -
m).
Theorem NZmul_0_l :
forall n :
Z, 0 *
n = 0.
Theorem NZmul_succ_l :
forall n m :
Z, (
NZsucc n) *
m =
n *
m +
m.
End NZAxiomsMod.
Definition NZlt :=
Zlt.
Definition NZle :=
Zle.
Definition NZmin :=
Zmin.
Definition NZmax :=
Zmax.
Add Morphism NZlt with signature NZeq ==>
NZeq ==>
iff as NZlt_wd.
Add Morphism NZle with signature NZeq ==>
NZeq ==>
iff as NZle_wd.
Add Morphism NZmin with signature NZeq ==>
NZeq ==>
NZeq as NZmin_wd.
Add Morphism NZmax with signature NZeq ==>
NZeq ==>
NZeq as NZmax_wd.
Theorem NZlt_eq_cases :
forall n m :
Z,
n <=
m <->
n <
m \/
n =
m.
Theorem NZlt_irrefl :
forall n :
Z, ~
n <
n.
Theorem NZlt_succ_r :
forall n m :
Z,
n < (
NZsucc m) <->
n <=
m.
Theorem NZmin_l :
forall n m :
NZ,
n <=
m ->
NZmin n m =
n.
Theorem NZmin_r :
forall n m :
NZ,
m <=
n ->
NZmin n m =
m.
Theorem NZmax_l :
forall n m :
NZ,
m <=
n ->
NZmax n m =
n.
Theorem NZmax_r :
forall n m :
NZ,
n <=
m ->
NZmax n m =
m.
End NZOrdAxiomsMod.
Definition Zopp (
x :
Z) :=
match x with
|
Z0 =>
Z0
|
Zpos x =>
Zneg x
|
Zneg x =>
Zpos x
end.
Add Morphism Zopp with signature NZeq ==>
NZeq as Zopp_wd.
Theorem Zsucc_pred :
forall n :
Z,
NZsucc (
NZpred n) =
n.
Theorem Zopp_0 : - 0 = 0.
Theorem Zopp_succ :
forall n :
Z, - (
NZsucc n) =
NZpred (-
n).
End ZBinAxiomsMod.
Module Export ZBinMulOrderPropMod :=
ZMulOrderPropFunct ZBinAxiomsMod.
Z forms a ring