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