Library Coq.Numbers.Integer.NatPairs.ZNatPairs
Require Import NSub.
Require Export ZMulOrder.
Require Export Ring.
Module ZPairsAxiomsMod (Import NAxiomsMod : NAxiomsSig) <: ZAxiomsSig.
Module Import NPropMod := NSubPropFunct NAxiomsMod.
Open Local Scope NatScope.
Lemma Nsemi_ring : semi_ring_theory 0 1 add mul Neq.
Add Ring NSR : Nsemi_ring.
Definition Z := (N * N)%type.
Definition Z0 : Z := (0, 0).
Definition Zeq (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)).
Definition Zsucc (n : Z) : Z := (S (fst n), snd n).
Definition Zpred (n : Z) : Z := (fst n, S (snd n)).
Definition Zadd (n m : Z) : Z := ((fst n) + (fst m), (snd n) + (snd m)).
Definition Zsub (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst m)).
Definition Zmul (n m : Z) : Z :=
((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)).
Definition Zlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n).
Definition Zle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n).
Definition Zmin (n m : Z) := (min ((fst n) + (snd m)) ((fst m) + (snd n)), (snd n) + (snd m)).
Definition Zmax (n m : Z) := (max ((fst n) + (snd m)) ((fst m) + (snd n)), (snd n) + (snd m)).
Delimit Scope IntScope with Int.
Notation "x == y" := (Zeq x y) (at level 70) : IntScope.
Notation "x ~= y" := (~ Zeq x y) (at level 70) : IntScope.
Notation "0" := Z0 : IntScope.
Notation "1" := (Zsucc Z0) : IntScope.
Notation "x + y" := (Zadd x y) : IntScope.
Notation "x - y" := (Zsub x y) : IntScope.
Notation "x * y" := (Zmul x y) : IntScope.
Notation "x < y" := (Zlt x y) : IntScope.
Notation "x <= y" := (Zle x y) : IntScope.
Notation "x > y" := (Zlt y x) (only parsing) : IntScope.
Notation "x >= y" := (Zle y x) (only parsing) : IntScope.
Notation Local N := NZ.
Notation Local NE := NZeq (only parsing).
Notation Local add_wd := NZadd_wd (only parsing).
Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
Module Export NZAxiomsMod <: NZAxiomsSig.
Definition NZ : Type := Z.
Definition NZeq := Zeq.
Definition NZ0 := Z0.
Definition NZsucc := Zsucc.
Definition NZpred := Zpred.
Definition NZadd := Zadd.
Definition NZsub := Zsub.
Definition NZmul := Zmul.
Theorem ZE_refl : reflexive Z Zeq.
Theorem ZE_sym : symmetric Z Zeq.
Theorem ZE_trans : transitive Z Zeq.
Theorem NZeq_equiv : equiv Z Zeq.
Add Relation Z Zeq
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 (@pair N N) with signature NE ==> NE ==> Zeq as Zpair_wd.
Add Morphism NZsucc with signature Zeq ==> Zeq as NZsucc_wd.
Add Morphism NZpred with signature Zeq ==> Zeq as NZpred_wd.
Add Morphism NZadd with signature Zeq ==> Zeq ==> Zeq as NZadd_wd.
Add Morphism NZsub with signature Zeq ==> Zeq ==> Zeq as NZsub_wd.
Add Morphism NZmul with signature Zeq ==> Zeq ==> Zeq as NZmul_wd.
Section Induction.
Open Scope NatScope.
Variable A : Z -> Prop.
Hypothesis A_wd : predicate_wd Zeq A.
Add Morphism A with signature Zeq ==> iff as A_morph.
Theorem NZinduction :
A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n.
End Induction.
Open Local Scope IntScope.
Theorem NZpred_succ : forall n : Z, Zpred (Zsucc n) == n.
Theorem NZadd_0_l : forall n : Z, 0 + n == n.
Theorem NZadd_succ_l : forall n m : Z, (Zsucc n) + m == Zsucc (n + m).
Theorem NZsub_0_r : forall n : Z, n - 0 == n.
Theorem NZsub_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m).
Theorem NZmul_0_l : forall n : Z, 0 * n == 0.
Theorem NZmul_succ_l : forall n m : Z, (Zsucc n) * m == n * m + m.
End NZAxiomsMod.
Definition NZlt := Zlt.
Definition NZle := Zle.
Definition NZmin := Zmin.
Definition NZmax := Zmax.
Add Morphism NZlt with signature Zeq ==> Zeq ==> iff as NZlt_wd.
Add Morphism NZle with signature Zeq ==> Zeq ==> iff as NZle_wd.
Add Morphism NZmin with signature Zeq ==> Zeq ==> Zeq as NZmin_wd.
Add Morphism NZmax with signature Zeq ==> Zeq ==> Zeq as NZmax_wd.
Open Local Scope IntScope.
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 < (Zsucc m) <-> n <= m.
Theorem NZmin_l : forall n m : Z, n <= m -> Zmin n m == n.
Theorem NZmin_r : forall n m : Z, m <= n -> Zmin n m == m.
Theorem NZmax_l : forall n m : Z, m <= n -> Zmax n m == n.
Theorem NZmax_r : forall n m : Z, n <= m -> Zmax n m == m.
End NZOrdAxiomsMod.
Definition Zopp (n : Z) : Z := (snd n, fst n).
Notation "- x" := (Zopp x) : IntScope.
Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd.
Open Local Scope IntScope.
Theorem Zsucc_pred : forall n : Z, Zsucc (Zpred n) == n.
Theorem Zopp_0 : - 0 == 0.
Theorem Zopp_succ : forall n, - (Zsucc n) == Zpred (- n).
End ZPairsAxiomsMod.