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