The following now compiles: abstract integers with plus, minus and times, binary implementation and integers as pairs of natural numbers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10167 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 394 insertions, 680 deletions

diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 0fd1be7a9..cb8ac3b5b 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -2,198 +2,174 @@ Require Import ZTimesOrder.
 Require Import ZArith.
 
 Open Local Scope Z_scope.
-Module Export ZBinDomain <: ZDomainSignature.
-Delimit Scope IntScope with Int.
-(* Is this really necessary? Without it, applying ZDomainProperties
-functor to this module produces an error since the functor opens the
-scope. *)
 
-Definition Z := Z.
-Definition E := (@eq Z).
-Definition e := Zeq_bool.
+Module ZBinAxiomsMod <: ZAxiomsSig.
+Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
+Module Export NZAxiomsMod <: NZAxiomsSig.
 
-Theorem E_equiv_e : forall x y : Z, E x y <-> e x y.
-Proof.
-intros x y; unfold E, e, Zeq_bool; split; intro H.
-rewrite H; now rewrite Zcompare_refl.
-rewrite eq_true_unfold_pos in H.
-assert (H1 : (x ?= y) = Eq).
-case_eq (x ?= y); intro H1; rewrite H1 in H; simpl in H;
-[reflexivity | discriminate H | discriminate H].
-now apply Zcompare_Eq_eq.
-Qed.
+Definition NZ := Z.
+Definition NZE := (@eq Z).
+Definition NZ0 := 0.
+Definition NZsucc := Zsucc'.
+Definition NZpred := Zpred'.
+Definition NZplus := Zplus.
+Definition NZminus := Zminus.
+Definition NZtimes := Zmult.
 
-Theorem E_equiv : equiv Z E.
+Theorem NZE_equiv : equiv Z NZE.
 Proof.
-apply eq_equiv with (A := Z). (* It does not work without "with (A := Z)" though it looks like it should *)
+exact (@eq_equiv Z).
 Qed.
 
-Add Relation Z E
- reflexivity proved by (proj1 E_equiv)
- symmetry proved by (proj2 (proj2 E_equiv))
- transitivity proved by (proj1 (proj2 E_equiv))
-as E_rel.
-
-End ZBinDomain.
+Add Relation Z NZE
+ reflexivity proved by (proj1 NZE_equiv)
+ symmetry proved by (proj2 (proj2 NZE_equiv))
+ transitivity proved by (proj1 (proj2 NZE_equiv))
+as NZE_rel.
 
-Module Export ZBinInt <: IntSignature.
-Module Export ZDomainModule := ZBinDomain.
-
-Definition O := 0.
-Definition S := Zsucc'.
-Definition P := Zpred'.
-
-Add Morphism S with signature E ==> E as S_wd.
+Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd.
 Proof.
-intros; unfold E; congruence.
-Qed.
-
-Add Morphism P with signature E ==> E as P_wd.
-Proof.
-intros; unfold E; congruence.
+congruence.
 Qed.
 
-Theorem S_inj : forall x y : Z, S x = S y -> x = y.
+Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd.
 Proof.
-exact Zsucc'_inj.
+congruence.
 Qed.
 
-Theorem S_P : forall x : Z, S (P x) = x.
+Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd.
 Proof.
-exact Zsucc'_pred'.
+congruence.
 Qed.
 
-Theorem induction :
-  forall Q : Z -> Prop,
-    pred_wd E Q -> Q 0 ->
-    (forall x, Q x -> Q (S x)) ->
-    (forall x, Q x -> Q (P x)) -> forall x, Q x.
+Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd.
 Proof.
-intros; now apply Zind.
+congruence.
 Qed.
 
-End ZBinInt.
-
-Module Export ZBinPlus <: ZPlusSignature.
-Module Export IntModule := ZBinInt.
-
-Definition plus := Zplus.
-Definition minus := Zminus.
-Definition uminus := Zopp.
-
-Add Morphism plus with signature E ==> E ==> E as plus_wd.
+Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd.
 Proof.
-intros; congruence.
+congruence.
 Qed.
 
-Add Morphism minus with signature E ==> E ==> E as minus_wd.
+Theorem NZpred_succ : forall n : Z, NZpred (NZsucc n) = n.
 Proof.
-intros; congruence.
+exact Zpred'_succ'.
 Qed.
 
-Add Morphism uminus with signature E ==> E as uminus_wd.
+Theorem NZinduction :
+  forall A : Z -> Prop, predicate_wd NZE A ->
+    A 0 -> (forall n : Z, A n <-> A (NZsucc n)) -> forall n : Z, A n.
 Proof.
-intros; congruence.
+intros A A_wd A0 AS n; apply Zind; clear n.
+assumption.
+intros; now apply -> AS.
+intros n H. rewrite <- (Zsucc'_pred' n) in H. now apply <- AS.
 Qed.
 
-Theorem plus_0 : forall n, 0 + n = n.
+Theorem NZplus_0_l : forall n : Z, 0 + n = n.
 Proof.
 exact Zplus_0_l.
 Qed.
 
-Theorem plus_S : forall n m, (S n) + m = S (n + m).
+Theorem NZplus_succ_l : forall n m : Z, (NZsucc n) + m = NZsucc (n + m).
 Proof.
 intros; do 2 rewrite <- Zsucc_succ'; apply Zplus_succ_l.
 Qed.
 
-Theorem minus_0 : forall n, n - 0 = n.
+Theorem NZminus_0_r : forall n : Z, n - 0 = n.
 Proof.
 exact Zminus_0_r.
 Qed.
 
-Theorem minus_S : forall n m, n - (S m) = P (n - m).
+Theorem NZminus_succ_r : forall n m : Z, n - (NZsucc m) = NZpred (n - m).
 Proof.
 intros; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred';
 apply Zminus_succ_r.
 Qed.
 
-Theorem uminus_0 : - 0 = 0.
+Theorem NZtimes_0_r : forall n : Z, n * 0 = 0.
 Proof.
-reflexivity.
+exact Zmult_0_r.
 Qed.
 
-Theorem uminus_S : forall n, - (S n) = P (- n).
-Admitted.
+Theorem NZtimes_succ_r : forall n m : Z, n * (NZsucc m) = n * m + n.
+Proof.
+intros; rewrite <- Zsucc_succ'; apply Zmult_succ_r.
+Qed.
 
-End ZBinPlus.
+End NZAxiomsMod.
 
-Module Export ZBinTimes <: ZTimesSignature.
-Module Export ZPlusModule := ZBinPlus.
+Definition NZlt := Zlt.
+Definition NZle := Zle.
 
-Definition times := Zmult.
+Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd.
+Proof.
+unfold NZE. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2.
+Qed.
 
-Add Morphism times with signature E ==> E ==> E as times_wd.
+Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd.
 Proof.
-congruence.
+unfold NZE. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2.
 Qed.
 
-Theorem times_0 : forall n, n * 0 = 0.
+Theorem NZle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n = m.
 Proof.
-exact Zmult_0_r.
+intros n m; split. apply Zle_lt_or_eq.
+intro H; destruct H as [H | H]. now apply Zlt_le_weak. rewrite H; apply Zle_refl.
 Qed.
 
-Theorem times_S : forall n m, n * (S m) = n * m + n.
+Theorem NZlt_irrefl : forall n : Z, ~ n < n.
 Proof.
-intros; rewrite <- Zsucc_succ'; apply Zmult_succ_r.
+exact Zlt_irrefl.
 Qed.
 
-End ZBinTimes.
+Theorem NZlt_succ_le : forall n m : Z, n < (NZsucc m) <-> n <= m.
+Proof.
+intros; unfold NZsucc; rewrite <- Zsucc_succ'; split;
+[apply Zlt_succ_le | apply Zle_lt_succ].
+Qed.
 
-Module Export ZBinOrder <: ZOrderSignature.
-Module Export IntModule := ZBinInt.
+End NZOrdAxiomsMod.
 
-Definition lt := Zlt_bool.
-Definition le := Zle_bool.
+Definition Zopp := Zopp.
 
-Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
+Add Morphism Zopp with signature NZE ==> NZE as Zopp_wd.
 Proof.
 congruence.
 Qed.
 
-Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
+Theorem Zsucc_pred : forall n : Z, NZsucc (NZpred n) = n.
 Proof.
-congruence.
+exact Zsucc'_pred'.
 Qed.
 
-Theorem le_lt : forall n m, le n m <-> lt n m \/ n = m.
+Theorem Zopp_0 : - 0 = 0.
 Proof.
-intros; unfold lt, le, Zlt_bool, Zle_bool.
-case_eq (n ?= m); intro H.
-apply Zcompare_Eq_eq in H; rewrite H; now split; intro; [right |].
-now split; intro; [left |].
-split; intro H1. now idtac.
-destruct H1 as [H1 | H1].
-assumption. unfold E in H1; rewrite H1 in H. now rewrite Zcompare_refl in H.
+reflexivity.
 Qed.
 
-Theorem lt_irr : forall n, ~ (lt n n).
+Theorem Zopp_succ : forall n : Z, - (NZsucc n) = NZpred (- n).
 Proof.
-intro n; rewrite eq_true_unfold_pos; intro H.
-assert (H1 : (Zlt n n)).
-change (if true then (Zlt n n) else (Zge n n)). rewrite <- H.
-unfold lt. apply Zlt_cases.
-false_hyp H1 Zlt_irrefl.
+intro; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred'. apply Zopp_succ.
 Qed.
 
-Theorem lt_S : forall n m, lt n (S m) <-> le n m.
-Proof.
-intros; unfold lt, le, S; do 2 rewrite eq_true_unfold_pos.
-rewrite <- Zsucc_succ'; rewrite <- Zlt_is_lt_bool; rewrite <- Zle_is_le_bool.
-split; intro; [now apply Zlt_succ_le | now apply Zle_lt_succ].
-Qed.
+End ZBinAxiomsMod.
+
+Module Export ZBinTimesOrderPropMod := ZTimesOrderPropFunct ZBinAxiomsMod.
 
-End ZBinOrder.
 
-Module Export ZTimesOrderPropertiesModule :=
-  ZTimesOrderProperties ZBinTimes ZBinOrder.
 
+
+(*
+Theorem E_equiv_e : forall x y : Z, E x y <-> e x y.
+Proof.
+intros x y; unfold E, e, Zeq_bool; split; intro H.
+rewrite H; now rewrite Zcompare_refl.
+rewrite eq_true_unfold_pos in H.
+assert (H1 : (x ?= y) = Eq).
+case_eq (x ?= y); intro H1; rewrite H1 in H; simpl in H;
+[reflexivity | discriminate H | discriminate H].
+now apply Zcompare_Eq_eq.
+Qed.
+*)
\ No newline at end of file
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
new file mode 100644
index 000000000..41fc7e75e
--- /dev/null
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -0,0 +1,303 @@
+Require Import NMinus. (* The most complete file for natural numbers *)
+Require Import ZTimesOrder. (* The most complete file for integers *)
+
+Module ZPairsAxiomsMod (Import NAxiomsMod : NAxiomsSig) <: ZAxiomsSig.
+Module Import NPropMod := NMinusPropFunct NAxiomsMod. (* Get all properties of natural numbers *)
+Notation Local N := NZ. (* To remember N without having to use a long qualifying name *)
+Notation Local NE := NZE (only parsing).
+Notation Local plus_wd := NZplus_wd (only parsing).
+Open Local Scope NatIntScope.
+
+Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
+Module Export NZAxiomsMod <: NZAxiomsSig.
+
+Definition NZ : Set := (NZ * NZ)%type.
+Definition NZE (p1 p2 : NZ) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)).
+Notation Z := NZ (only parsing).
+Notation E := NZE (only parsing).
+Definition NZ0 := (0, 0).
+Definition NZsucc (n : Z) := (S (fst n), snd n).
+Definition NZpred (n : Z) := (fst n, S (snd n)).
+(* We do not have P (S n) = n but only P (S n) == n. It could be possible
+to consider as canonical only pairs where one of the elements is 0, and
+make all operations convert canonical values into other canonical values.
+In that case, we could get rid of setoids as well as arrive at integers as
+signed natural numbers. *)
+Definition NZplus (n m : Z) := ((fst n) + (fst m), (snd n) + (snd m)).
+Definition NZminus (n m : Z) := ((fst n) + (snd m), (snd n) + (fst m)).
+Definition NZuminus (n : Z) := (snd n, fst n).
+(* Unfortunately, the elements of the pair keep increasing, even during
+subtraction *)
+Definition NZtimes (n m : Z) :=
+  ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)).
+
+Theorem ZE_refl : reflexive Z E.
+Proof.
+unfold reflexive, E; reflexivity.
+Qed.
+
+Theorem ZE_symm : symmetric Z E.
+Proof.
+unfold symmetric, E; now symmetry.
+Qed.
+
+Theorem ZE_trans : transitive Z E.
+Proof.
+unfold transitive, E. intros n m p H1 H2.
+assert (H3 : (fst n + snd m) + (fst m + snd p) == (fst m + snd n) + (fst p + snd m))
+by now apply plus_wd.
+stepl ((fst n + snd p) + (fst m + snd m)) in H3 by ring.
+stepr ((fst p + snd n) + (fst m + snd m)) in H3 by ring.
+now apply -> plus_cancel_r in H3.
+Qed.
+
+Theorem NZE_equiv : equiv Z E.
+Proof.
+unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_symm].
+Qed.
+
+Add Relation Z E
+ reflexivity proved by (proj1 NZE_equiv)
+ symmetry proved by (proj2 (proj2 NZE_equiv))
+ transitivity proved by (proj1 (proj2 NZE_equiv))
+as NZE_rel.
+
+Add Morphism (@pair N N) with signature NE ==> NE ==> E as Zpair_wd.
+Proof.
+intros n1 n2 H1 m1 m2 H2; unfold E; simpl; rewrite H1; now rewrite H2.
+Qed.
+
+Add Morphism NZsucc with signature E ==> E as NZsucc_wd.
+Proof.
+unfold NZsucc, E; intros n m H; simpl.
+do 2 rewrite plus_succ_l; now rewrite H.
+Qed.
+
+Add Morphism NZpred with signature E ==> E as NZpred_wd.
+Proof.
+unfold NZpred, E; intros n m H; simpl.
+do 2 rewrite plus_succ_r; now rewrite H.
+Qed.
+
+Add Morphism NZplus with signature E ==> E ==> E as NZplus_wd.
+Proof.
+unfold E, NZplus; intros n1 m1 H1 n2 m2 H2; simpl.
+assert (H3 : (fst n1 + snd m1) + (fst n2 + snd m2) == (fst m1 + snd n1) + (fst m2 + snd n2))
+by now apply plus_wd.
+stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring.
+now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring.
+Qed.
+
+Add Morphism NZminus with signature E ==> E ==> E as NZminus_wd.
+Proof.
+unfold E, NZminus; intros n1 m1 H1 n2 m2 H2; simpl.
+symmetry in H2.
+assert (H3 : (fst n1 + snd m1) + (fst m2 + snd n2) == (fst m1 + snd n1) + (fst n2 + snd m2))
+by now apply plus_wd.
+stepl (fst n1 + snd m1 + (fst m2 + snd n2)) by ring.
+now stepr (fst m1 + snd n1 + (fst n2 + snd m2)) by ring.
+Qed.
+
+Add Morphism NZtimes with signature E ==> E ==> E as NZtimes_wd.
+Proof.
+unfold NZtimes, E; intros n1 m1 H1 n2 m2 H2; simpl.
+stepl (fst n1 * fst n2 + (snd n1 * snd n2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
+stepr (fst n1 * snd n2 + (fst m1 * fst m2 + snd m1 * snd m2 + snd n1 * fst n2)) by ring.
+apply plus_times_repl_pair with (n := fst m2) (m := snd m2); [| now idtac].
+stepl (snd n1 * snd n2 + (fst n1 * fst m2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
+stepr (snd n1 * fst n2 + (fst n1 * snd m2 + fst m1 * fst m2 + snd m1 * snd m2)) by ring.
+apply plus_times_repl_pair with (n := snd m2) (m := fst m2);
+[| (stepl (fst n2 + snd m2) by ring); now stepr (fst m2 + snd n2) by ring].
+stepl (snd m2 * snd n1 + (fst n1 * fst m2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
+stepr (snd m2 * fst n1 + (snd n1 * fst m2 + fst m1 * fst m2 + snd m1 * snd m2)) by ring.
+apply plus_times_repl_pair with (n := snd m1) (m := fst m1);
+[ | (stepl (fst n1 + snd m1) by ring); now stepr (fst m1 + snd n1) by ring].
+stepl (fst m2 * fst n1 + (snd m2 * snd m1 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
+stepr (fst m2 * snd n1 + (snd m2 * fst m1 + fst m1 * fst m2 + snd m1 * snd m2)) by ring.
+apply plus_times_repl_pair with (n := fst m1) (m := snd m1); [| now idtac].
+ring.
+Qed.
+
+Delimit Scope IntScope with Int.
+Bind Scope IntScope with NZ.
+Open Local Scope IntScope.
+Notation "x == y"  := (NZE x y) (at level 70) : IntScope.
+Notation "x ~= y" := (~ NZE x y) (at level 70) : IntScope.
+Notation "0" := NZ0 : IntScope.
+Notation "'S'" := NZsucc : IntScope.
+Notation "'P'" := NZpred : IntScope.
+Notation "1" := (S 0) : IntScope.
+Notation "x + y" := (NZplus x y) : IntScope.
+Notation "x - y" := (NZminus x y) : IntScope.
+Notation "x * y" := (NZtimes x y) : IntScope.
+
+Theorem NZpred_succ : forall n : Z, P (S n) == n.
+Proof.
+unfold NZpred, NZsucc, E; intro n; simpl.
+rewrite plus_succ_l; now rewrite plus_succ_r.
+Qed.
+
+Section Induction.
+Open Scope NatIntScope. (* automatically closes at the end of the section *)
+Variable A : Z -> Prop.
+Hypothesis A_wd : predicate_wd E A.
+
+Add Morphism A with signature E ==> iff as A_morph.
+Proof.
+exact A_wd.
+Qed.
+
+Theorem NZinduction :
+  A 0 -> (forall n : Z, A n <-> A (S n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *)
+Proof.
+intros A0 AS n; unfold NZ0, NZsucc, predicate_wd, fun_wd, E in *.
+destruct n as [n m].
+cut (forall p : N, A (p, 0)); [intro H1 |].
+cut (forall p : N, A (0, p)); [intro H2 |].
+destruct (plus_dichotomy n m) as [[p H] | [p H]].
+rewrite (A_wd (n, m) (0, p)); simpl. rewrite plus_0_l; now rewrite plus_comm. apply H2.
+rewrite (A_wd (n, m) (p, 0)); simpl. now rewrite plus_0_r. apply H1.
+induct p. assumption. intros p IH.
+apply -> (A_wd (0, p) (1, S p)) in IH; [| now rewrite plus_0_l, plus_1_l].
+now apply <- AS.
+induct p. assumption. intros p IH.
+replace 0 with (snd (p, 0)); [| reflexivity].
+replace (S p) with (S (fst (p, 0))); [| reflexivity]. now apply -> AS.
+Qed.
+
+End Induction.
+
+Theorem NZplus_0_l : forall n : Z, 0 + n == n.
+Proof.
+intro n; unfold NZplus, E; simpl. now do 2 rewrite plus_0_l.
+Qed.
+
+Theorem NZplus_succ_l : forall n m : Z, (S n) + m == S (n + m).
+Proof.
+intros n m; unfold NZplus, E; simpl. now do 2 rewrite plus_succ_l.
+Qed.
+
+Theorem NZminus_0_r : forall n : Z, n - 0 == n.
+Proof.
+intro n; unfold NZminus, E; simpl. now do 2 rewrite plus_0_r.
+Qed.
+
+Theorem NZminus_succ_r : forall n m : Z, n - (S m) == P (n - m).
+Proof.
+intros n m; unfold NZminus, E; simpl. symmetry; now rewrite plus_succ_r.
+Qed.
+
+Theorem NZtimes_0_r : forall n : Z, n * 0 == 0.
+Proof.
+intro n; unfold NZtimes, E; simpl.
+repeat rewrite times_0_r. now rewrite plus_assoc.
+Qed.
+
+Theorem NZtimes_succ_r : forall n m : Z, n * (S m) == n * m + n.
+Proof.
+intros n m; unfold NZtimes, NZsucc, E; simpl.
+do 2 rewrite times_succ_r. ring.
+Qed.
+
+End NZAxiomsMod.
+
+Definition NZlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n).
+Definition NZle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n).
+
+Notation "x < y" := (NZlt x y) : IntScope.
+Notation "x <= y" := (NZle x y) : IntScope.
+Notation "x > y" := (NZlt y x) (only parsing) : IntScope.
+Notation "x >= y" := (NZle y x) (only parsing) : IntScope.
+
+Add Morphism NZlt with signature E ==> E ==> iff as NZlt_wd.
+Proof.
+unfold NZlt, E; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H.
+stepr (snd m1 + fst m2) by apply plus_comm.
+apply (plus_lt_repl_pair (fst n1) (snd n1)); [| assumption].
+stepl (snd m2 + fst n1) by apply plus_comm.
+stepr (fst m2 + snd n1) by apply plus_comm.
+apply (plus_lt_repl_pair (snd n2) (fst n2)).
+now stepl (fst n1 + snd n2) by apply plus_comm.
+stepl (fst m2 + snd n2) by apply plus_comm. now stepr (fst n2 + snd m2) by apply plus_comm.
+stepr (snd n1 + fst n2) by apply plus_comm.
+apply (plus_lt_repl_pair (fst m1) (snd m1)); [| now symmetry].
+stepl (snd n2 + fst m1) by apply plus_comm.
+stepr (fst n2 + snd m1) by apply plus_comm.
+apply (plus_lt_repl_pair (snd m2) (fst m2)).
+now stepl (fst m1 + snd m2) by apply plus_comm.
+stepl (fst n2 + snd m2) by apply plus_comm. now stepr (fst m2 + snd n2) by apply plus_comm.
+Qed.
+
+Open Local Scope IntScope.
+
+Add Morphism NZle with signature E ==> E ==> iff as NZle_wd.
+Proof.
+unfold NZle, E; intros n1 m1 H1 n2 m2 H2; simpl.
+do 2 rewrite le_lt_or_eq. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2).
+fold (n1 == n2) (m1 == m2); fold (n1 == m1) in H1; fold (n2 == m2) in H2.
+now rewrite H1, H2.
+Qed.
+
+Theorem NZle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m.
+Proof.
+intros n m; unfold NZlt, NZle, E; simpl. apply le_lt_or_eq.
+Qed.
+
+Theorem NZlt_irrefl : forall n : Z, ~ (n < n).
+Proof.
+intros n; unfold NZlt, E; simpl. apply lt_irrefl.
+Qed.
+
+Theorem NZlt_succ_le : forall n m : Z, n < (S m) <-> n <= m.
+Proof.
+intros n m; unfold NZlt, NZle, E; simpl. rewrite plus_succ_l; apply lt_succ_le.
+Qed.
+
+End NZOrdAxiomsMod.
+
+Definition Zopp (n : Z) := (snd n, fst n).
+
+Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope.
+
+Add Morphism Zopp with signature E ==> E as Zopp_wd.
+Proof.
+unfold E; intros n m H; simpl. symmetry.
+stepl (fst n + snd m) by apply plus_comm.
+now stepr (fst m + snd n) by apply plus_comm.
+Qed.
+
+Open Local Scope IntScope.
+
+Theorem Zsucc_pred : forall n : Z, S (P n) == n.
+Proof.
+intro n; unfold NZsucc, NZpred, E; simpl.
+rewrite plus_succ_l; now rewrite plus_succ_r.
+Qed.
+
+Theorem Zopp_0 : - 0 == 0.
+Proof.
+unfold Zopp, E; simpl. now rewrite plus_0_l.
+Qed.
+
+Theorem Zopp_succ : forall n, - (S n) == P (- n).
+Proof.
+reflexivity.
+Qed.
+
+End ZPairsAxiomsMod.
+
+(* For example, let's build integers out of pairs of Peano natural numbers
+and get their properties *)
+
+(* The following lines increase the compilation time at least twice *)
+(*
+Require Import NPeano.
+
+Module Export ZPairsPeanoAxiomsMod := ZPairsAxiomsMod NPeanoAxiomsMod.
+Module Export ZPairsTimesOrderPropMod := ZTimesOrderPropFunct ZPairsPeanoAxiomsMod.
+
+Open Local Scope IntScope.
+
+Eval compute in (3, 5) * (4, 6).
+*)
+
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
deleted file mode 100644
index 2a9b4f386..000000000
--- a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
+++ /dev/null
@@ -1,142 +0,0 @@
-Require Import NPlus.
-Require Export ZAxioms.
-
-Module NatPairsDomain (Import NPlusMod : NPlusSig) <: ZDomainSignature.
-(*  with Definition Z :=
-    (NPM.NBaseMod.DomainModule.N * NPM.NBaseMod.DomainModule.N)%type
-  with Definition E :=
-    fun p1 p2  =>
-      NPM.NBaseMod.DomainModule.E (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1))
-  with Definition e :=
-    fun p1 p2  =>
-      NPM.NBaseMod.DomainModule.e (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1)).*)
-
-Module Export NPlusPropMod := NPlusPropFunct NBaseMod NPlusMod.
-Open Local Scope NatScope.
-
-Definition Z : Set := (N * N)%type.
-Definition E (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)).
-Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1)).
-
-Delimit Scope IntScope with Int.
-Bind Scope IntScope with Z.
-Notation "x == y" := (E x y) (at level 70) : IntScope.
-Notation "x # y" := (~ E x y) (at level 70) : IntScope.
-
-Theorem E_equiv_e : forall x y : Z, E x y <-> e x y.
-Proof.
-intros x y; unfold E, e; apply E_equiv_e.
-Qed.
-
-Theorem ZE_refl : reflexive Z E.
-Proof.
-unfold reflexive, E; reflexivity.
-Qed.
-
-Theorem ZE_symm : symmetric Z E.
-Proof.
-unfold symmetric, E; now symmetry.
-Qed.
-
-Theorem ZE_trans : transitive Z E.
-Proof.
-unfold transitive, E. intros x y z H1 H2.
-apply plus_cancel_l with (p := fst y + snd y).
-rewrite (plus_shuffle2 (fst y) (snd y) (fst x) (snd z)).
-rewrite (plus_shuffle2 (fst y) (snd y) (fst z) (snd x)).
-rewrite plus_comm. rewrite (plus_comm (snd y) (fst x)).
-rewrite (plus_comm (snd y) (fst z)). now apply plus_wd.
-Qed.
-
-Theorem E_equiv : equiv Z E.
-Proof.
-unfold equiv; split; [apply ZE_refl | split; [apply ZE_trans | apply ZE_symm]].
-Qed.
-
-Add Relation Z E
- reflexivity proved by (proj1 E_equiv)
- symmetry proved by (proj2 (proj2 E_equiv))
- transitivity proved by (proj1 (proj2 E_equiv))
-as E_rel.
-
-Add Morphism (@pair N N)
-  with signature NDomainModule.E ==> NDomainModule.E ==> E
-  as pair_wd.
-Proof.
-intros x1 x2 H1 y1 y2 H2; unfold E; simpl; rewrite H1; now rewrite H2.
-Qed.
-
-End NatPairsDomain.
-
-Module NatPairsInt (Import NPlusMod : NPlusSig) <: ZBaseSig.
-Module Export ZDomainModule := NatPairsDomain NPlusMod.
-Module Export ZDomainModuleProperties := ZDomainProperties ZDomainModule.
-Open Local Scope IntScope.
-
-Definition O : Z := (0, 0)%Nat.
-Definition S (n : Z) := (NBaseMod.S (fst n), snd n).
-Definition P (n : Z) := (fst n, NBaseMod.S (snd n)).
-(* Unfortunately, we do not have P (S n) = n but only P (S n) == n.
-It could be possible to consider as "canonical" only pairs where one of
-the elements is 0, and make all operations convert canonical values into
-other canonical values. We do not do this because this is more complex
-and because we do not have the predecessor function on N at this point. *)
-
-Notation "0" := O : IntScope.
-
-Add Morphism S with signature E ==> E as succ_wd.
-Proof.
-unfold S, E; intros n m H; simpl.
-do 2 rewrite plus_succ_l; now rewrite H.
-Qed.
-
-Add Morphism P with signature E ==> E as pred_wd.
-Proof.
-unfold P, E; intros n m H; simpl.
-do 2 rewrite plus_succ_r; now rewrite H.
-Qed.
-
-Theorem succ_inj : forall x y : Z, S x == S y -> x == y.
-Proof.
-unfold S, E; simpl; intros x y H.
-do 2 rewrite plus_succ_l in H. now apply succ_inj in H.
-Qed.
-
-Theorem succ_pred : forall x : Z, S (P x) == x.
-Proof.
-intro x; unfold S, P, E; simpl.
-rewrite plus_succ_l; now rewrite plus_succ_r.
-Qed.
-
-Section Induction.
-Open Scope NatScope. (* automatically closes at the end of the section *)
-Variable A : Z -> Prop.
-Hypothesis Q_wd : predicate_wd E A.
-
-Add Morphism A with signature E ==> iff as Q_morph.
-Proof.
-exact Q_wd.
-Qed.
-
-Theorem induction :
-  A 0 -> (forall x, A x -> A (S x)) -> (forall x, A x -> A (P x)) -> forall x, A x.
-Proof.
-intros Q0 QS QP x; unfold O, S, P, predicate_wd, E in *.
-destruct x as [n m].
-cut (forall p : N, A (p, 0)); [intro H1 |].
-cut (forall p : N, A (0, p)); [intro H2 |].
-destruct (plus_dichotomy n m) as [[p H] | [p H]].
-rewrite (Q_wd (n, m) (0, p)); simpl. rewrite plus_0_l; now rewrite plus_comm. apply H2.
-rewrite (Q_wd (n, m) (p, 0)); simpl. now rewrite plus_0_r. apply H1.
-induct p. assumption. intros p IH.
-replace 0 with (fst (0, p)); [| reflexivity].
-replace p with (snd (0, p)); [| reflexivity]. now apply QP.
-induct p. assumption. intros p IH.
-replace 0 with (snd (p, 0)); [| reflexivity].
-replace p with (fst (p, 0)); [| reflexivity]. now apply QS.
-Qed.
-
-End Induction.
-
-End NatPairsInt.
-
diff --git a/theories/Numbers/NatInt/NZOrder1.v b/theories/Numbers/NatInt/NZOrder1.v
deleted file mode 100644
index 6a15ddc6a..000000000
--- a/theories/Numbers/NatInt/NZOrder1.v
+++ /dev/null
@@ -1,423 +0,0 @@
-Require Export NZBase.
-
-Module Type NZOrderSig.
-Declare Module Export NZBaseMod : NZBaseSig.
-
-Parameter Inline NZlt : NZ -> NZ -> Prop.
-Parameter Inline NZle : NZ -> NZ -> Prop.
-
-Axiom NZlt_wd : rel_wd NZE NZE NZlt.
-Axiom NZle_wd : rel_wd NZE NZE NZle.
-
-Notation "x < y" := (NZlt x y).
-Notation "x <= y" := (NZle x y).
-
-Axiom NZle__lt_or_eq : forall n m : NZ, n <= m <-> n < m \/ n == m.
-Axiom NZlt_irrefl : forall n : NZ, ~ (n < n).
-Axiom NZlt_succ__le : forall n m : NZ, n < S m <-> n <= m.
-End NZOrderSig.
-
-Module NZOrderPropFunct (Import NZOrderMod : NZOrderSig).
-Module Export NZBasePropMod := NZBasePropFunct NZBaseMod.
-
-Ltac NZle_intro1 := rewrite NZle__lt_or_eq; left.
-Ltac NZle_intro2 := rewrite NZle__lt_or_eq; right.
-Ltac NZle_elim H := rewrite NZle__lt_or_eq in H; destruct H as [H | H].
-
-Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_morph.
-Proof.
-exact NZlt_wd.
-Qed.
-
-Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_morph.
-Proof.
-exact NZle_wd.
-Qed.
-
-Lemma NZlt_stepl : forall x y z : NZ, x < y -> x == z -> z < y.
-Proof.
-intros x y z H1 H2; now rewrite <- H2.
-Qed.
-
-Lemma NZlt_stepr : forall x y z : NZ, x < y -> y == z -> x < z.
-Proof.
-intros x y z H1 H2; now rewrite <- H2.
-Qed.
-
-Lemma NZle_stepl : forall x y z : NZ, x <= y -> x == z -> z <= y.
-Proof.
-intros x y z H1 H2; now rewrite <- H2.
-Qed.
-
-Lemma NZle_stepr : forall x y z : NZ, x <= y -> y == z -> x <= z.
-Proof.
-intros x y z H1 H2; now rewrite <- H2.
-Qed.
-
-Declare Left  Step NZlt_stepl.
-Declare Right Step NZlt_stepr.
-Declare Left  Step NZle_stepl.
-Declare Right Step NZle_stepr.
-
-Theorem NZlt_le_incl : forall n m : NZ, n < m -> n <= m.
-Proof.
-intros; now NZle_intro1.
-Qed.
-
-Theorem NZlt_neq : forall n m : NZ, n < m -> n ~= m.
-Proof.
-intros n m H1 H2; rewrite H2 in H1; false_hyp H1 NZlt_irrefl.
-Qed.
-
-Theorem NZle_refl : forall n : NZ, n <= n.
-Proof.
-intro; now NZle_intro2.
-Qed.
-
-Theorem NZlt_succ_r : forall n : NZ, n < S n.
-Proof.
-intro n. rewrite NZlt_succ__le. now NZle_intro2.
-Qed.
-
-Theorem NZle_succ_r : forall n : NZ, n <= S n.
-Proof.
-intro; NZle_intro1; apply NZlt_succ_r.
-Qed.
-
-Theorem NZlt__lt_succ : forall n m : NZ, n < m -> n < S m.
-Proof.
-intros. rewrite NZlt_succ__le. now NZle_intro1.
-Qed.
-
-Theorem NZle__le_succ : forall n m : NZ, n <= m -> n <= S m.
-Proof.
-intros n m H; rewrite <- NZlt_succ__le in H; now NZle_intro1.
-Qed.
-
-Theorem NZle_succ__le_or_eq_succ : forall n m : NZ, n <= S m <-> n <= m \/ n == S m.
-Proof.
-intros n m; rewrite NZle__lt_or_eq. now rewrite NZlt_succ__le.
-Qed.
-
-(** A corollary of having an order is that NZ is infinite *)
-
-(* This section about infinity of NZ relies on the type nat and can be
-safely removed *)
-
-Definition succ_iter (n : nat) (m : NZ) :=
-  nat_rec (fun _ => NZ) m (fun _ l => S l) n.
-
-Theorem NZlt_succ_iter_r :
-  forall (n : nat) (m : NZ), m < succ_iter (Datatypes.S n) m.
-Proof.
-intros n m; induction n as [| n IH]; simpl in *.
-apply NZlt_succ_r. now apply NZlt__lt_succ.
-Qed.
-
-Theorem NZneq_succ_iter_l :
-  forall (n : nat) (m : NZ), succ_iter (Datatypes.S n) m ~= m.
-Proof.
-intros n m H. pose proof (NZlt_succ_iter_r n m) as H1. rewrite H in H1.
-false_hyp H1 NZlt_irrefl.
-Qed.
-
-(* End of the section about the infinity of NZ *)
-
-(* The following theorem is a special case of NZneq_succ_iter_l, but we
-prove it independently *)
-
-Theorem NZneq_succ_l : forall n : NZ, S n ~= n.
-Proof.
-intros n H. pose proof (NZlt_succ_r n) as H1. rewrite H in H1.
-false_hyp H1 NZlt_irrefl.
-Qed.
-
-Theorem NZnlt_succ_l : forall n : NZ, ~ S n < n.
-Proof.
-intros n H; apply NZlt__lt_succ in H. false_hyp H NZlt_irrefl.
-Qed.
-
-Theorem NZnle_succ_l : forall n : NZ, ~ S n <= n.
-Proof.
-intros n H; NZle_elim H.
-false_hyp H NZnlt_succ_l. false_hyp H NZneq_succ_l.
-Qed.
-
-Theorem NZlt__le_succ : forall n m : NZ, n < m <-> S n <= m.
-Proof.
-intro n; NZinduct_center m n.
-rewrite_false (n < n) NZlt_irrefl. now rewrite_false (S n <= n) NZnle_succ_l.
-intro m. rewrite NZlt_succ__le. rewrite NZle_succ__le_or_eq_succ.
-rewrite NZsucc_inj_wd. rewrite (NZle__lt_or_eq n m).
-rewrite or_cancel_r.
-apply NZlt_neq.
-intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_l.
-reflexivity.
-Qed.
-
-Theorem NZlt_succ__lt : forall n m : NZ, S n < m -> n < m.
-Proof.
-intros n m H; apply <- NZlt__le_succ; now NZle_intro1.
-Qed.
-
-Theorem NZle_succ__le : forall n m : NZ, S n <= m -> n <= m.
-Proof.
-intros n m H; NZle_intro1; now apply <- NZlt__le_succ.
-Qed.
-
-Theorem NZsucc_lt_mono : forall n m : NZ, n < m <-> S n < S m.
-Proof.
-intros n m. rewrite NZlt__le_succ. symmetry. apply NZlt_succ__le.
-Qed.
-
-Theorem NZsucc_le_mono : forall n m : NZ, n <= m <-> S n <= S m.
-Proof.
-intros n m. do 2 rewrite NZle__lt_or_eq.
-rewrite <- NZsucc_lt_mono; now rewrite NZsucc_inj_wd.
-Qed.
-
-Theorem NZlt_lt_false : forall n m, n < m -> m < n -> False.
-Proof.
-intros n m; NZinduct_center n m.
-intros H _; false_hyp H NZlt_irrefl.
-intro n; split; intros H H1 H2.
-apply NZlt_succ__lt in H1. apply -> NZlt_succ__le in H2. NZle_elim H2.
-now apply H. rewrite H2 in H1; false_hyp H1 NZlt_irrefl.
-apply NZlt__lt_succ in H2. apply -> NZlt__le_succ in H1. NZle_elim H1.
-now apply H. rewrite H1 in H2; false_hyp H2 NZlt_irrefl.
-Qed.
-
-Theorem NZlt_asymm : forall n m, n < m -> ~ m < n.
-Proof.
-intros n m; unfold not; apply NZlt_lt_false.
-Qed.
-
-Theorem NZlt_trans : forall n m p : NZ, n < m -> m < p -> n < p.
-Proof.
-intros n m p; NZinduct_center p m.
-intros _ H; false_hyp H NZlt_irrefl.
-intro p. do 2 rewrite NZlt_succ__le.
-split; intros H H1 H2.
-NZle_intro1; NZle_elim H2; [now apply H | now rewrite H2 in H1].
-assert (n <= p) as H3. apply H. assumption. now NZle_intro1.
-NZle_elim H3. assumption. rewrite <- H3 in H2. elimtype False.
-now apply (NZlt_lt_false n m).
-Qed.
-
-Theorem NZle_trans : forall n m p : NZ, n <= m -> m <= p -> n <= p.
-Proof.
-intros n m p H1 H2; NZle_elim H1.
-NZle_elim H2. NZle_intro1; now apply NZlt_trans with (m := m).
-NZle_intro1; now rewrite <- H2. now rewrite H1.
-Qed.
-
-Theorem NZle_lt_trans : forall n m p : NZ, n <= m -> m < p -> n < p.
-Proof.
-intros n m p H1 H2; NZle_elim H1.
-now apply NZlt_trans with (m := m). now rewrite H1.
-Qed.
-
-Theorem NZlt_le_trans : forall n m p : NZ, n < m -> m <= p -> n < p.
-Proof.
-intros n m p H1 H2; NZle_elim H2.
-now apply NZlt_trans with (m := m). now rewrite <- H2.
-Qed.
-
-Theorem NZle_antisym : forall n m : NZ, n <= m -> m <= n -> n == m.
-Proof.
-intros n m H1 H2; now (NZle_elim H1; NZle_elim H2);
-[elimtype False; apply (NZlt_lt_false n m) | | |].
-Qed.
-
-(** Trichotomy, decidability, and double negation elimination *)
-
-Theorem NZlt_trichotomy : forall n m : NZ,  n < m \/ n == m \/ m < n.
-Proof.
-intros n m; NZinduct_center n m.
-right; now left.
-intro n; rewrite NZlt_succ__le. stepr ((S n < m \/ S n == m) \/ m <= n) by tauto.
-rewrite <- (NZle__lt_or_eq (S n) m). symmetry (n == m).
-stepl (n < m \/ m < n \/ m == n) by tauto. rewrite <- NZle__lt_or_eq.
-apply or_iff_compat_r. apply NZlt__le_succ.
-Qed.
-
-Theorem NZle_lt_dec : forall n m : NZ, n <= m \/ m < n.
-Proof.
-intros n m; destruct (NZlt_trichotomy n m) as [H | [H | H]].
-left; now NZle_intro1. left; now NZle_intro2. now right.
-Qed.
-
-Theorem NZle_nlt : forall n m : NZ, n <= m <-> ~ m < n.
-Proof.
-intros n m. split; intro H; [intro H1 |].
-eapply NZle_lt_trans in H; [| eassumption ..]. false_hyp H NZlt_irrefl.
-destruct (NZle_lt_dec n m) as [H1 | H1].
-assumption. false_hyp H1 H.
-Qed.
-
-Theorem NZlt_dec : forall n m : NZ, n < m \/ ~ n < m.
-Proof.
-intros n m; destruct (NZle_lt_dec m n);
-[right; now apply -> NZle_nlt | now left].
-Qed.
-
-Theorem NZlt_dne : forall n m, ~ ~ n < m <-> n < m.
-Proof.
-intros n m; split; intro H;
-[destruct (NZlt_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] |
-intro H1; false_hyp H H1].
-Qed.
-
-Theorem NZnle_lt : forall n m : NZ, ~ n <= m <-> m < n.
-Proof.
-intros n m. rewrite NZle_nlt. apply NZlt_dne.
-Qed.
-
-Theorem NZle_dec : forall n m : NZ, n <= m \/ ~ n <= m.
-Proof.
-intros n m; destruct (NZle_lt_dec n m);
-[now left | right; now apply <- NZnle_lt].
-Qed.
-
-Theorem NZle_dne : forall n m : NZ, ~ ~ n <= m <-> n <= m.
-Proof.
-intros n m; split; intro H;
-[destruct (NZle_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] |
-intro H1; false_hyp H H1].
-Qed.
-
-Theorem NZlt__nlt_succ : forall n m : NZ, n < m <-> ~ m < S n.
-Proof.
-intros n m; rewrite NZlt_succ__le; symmetry; apply NZnle_lt.
-Qed.
-
-(** Stronger variant of induction with assumptions n >= 0 (n <= 0)
-in the induction step *)
-
-Section Induction.
-
-Variable A : Z -> Prop.
-Hypothesis Q_wd : predicate_wd NZE A.
-
-Add Morphism A with signature NZE ==> iff as Q_morph.
-Proof Q_wd.
-
-Section Center.
-
-Variable z : Z. (* A z is the basis of induction *)
-
-Section RightInduction.
-
-Let Q' := fun n : Z => forall m : NZ, z <= m -> m < n -> A m.
-
-Add Morphism Q' with signature NZE ==> iff as Q'_pos_wd.
-Proof.
-intros x1 x2 H; unfold Q'; qmorphism x1 x2.
-Qed.
-
-Theorem NZright_induction :
-  A z -> (forall n : NZ, z <= n -> A n -> A (S n)) -> forall n : NZ, z <= n -> A n.
-Proof.
-intros Qz QS k k_ge_z.
-assert (H : forall n : NZ, Q' n). induct_n n z; unfold Q'.
-intros m H1 H2. apply -> le_gt in H1; false_hyp H2 H1.
-intros n IH m H2 H3.
-rewrite NZlt_succ in H3; Zle_elim H3. now apply IH.
-Zle_elim H2. rewrite_succ_pred m.
-apply QS. now apply -> lt_n_m_pred. apply IH. now apply -> lt_n_m_pred.
-rewrite H3; apply NZlt_pred_l. now rewrite <- H2.
-intros n IH m H2 H3. apply IH. assumption. now apply lt_n_predm.
-pose proof (H (S k)) as H1; unfold Q' in H1. apply H1.
-apply k_ge_z. apply NZlt_succ_r.
-Qed.
-
-End RightInduction.
-
-Section LeftInduction.
-
-Let Q' := fun n : Z => forall m : NZ, m <= z -> n < m -> A m.
-
-Add Morphism Q' with signature NZE ==> iff as Q'_neg_wd.
-Proof.
-intros x1 x2 H; unfold Q'; qmorphism x1 x2.
-Qed.
-
-Theorem NZleft_induction :
-  A z -> (forall n : NZ, n <= z -> A n -> A (P n)) -> forall n : NZ, n <= z -> A n.
-Proof.
-intros Qz QP k k_le_z.
-assert (H : forall n : NZ, Q' n). induct_n n z; unfold Q'.
-intros m H1 H2. apply -> le_gt in H1; false_hyp H2 H1.
-intros n IH m H2 H3. apply IH. assumption. now apply lt_succ__lt.
-intros n IH m H2 H3.
-rewrite NZlt_pred in H3; Zle_elim H3. now apply IH.
-Zle_elim H2. rewrite_pred_succ m.
-apply QP. now apply -> lt_n_m_succ. apply IH. now apply -> lt_n_m_succ.
-rewrite H3; apply NZlt_succ_r. now rewrite H2.
-pose proof (H (P k)) as H1; unfold Q' in H1. apply H1.
-apply k_le_z. apply NZlt_pred_l.
-Qed.
-
-End LeftInduction.
-
-Theorem NZinduction_ord_n :
-  A z ->
-  (forall n : NZ, z <= n -> A n -> A (S n)) ->
-  (forall n : NZ, n <= z -> A n -> A (P n)) ->
-    forall n : NZ, A n.
-Proof.
-intros Qz QS QP n.
-destruct (lt_total n z) as [H | [H | H]].
-now apply left_induction; [| | Zle_intro1].
-now rewrite H.
-now apply right_induction; [| | Zle_intro1].
-Qed.
-
-End Center.
-
-Theorem NZinduction_ord :
-  A 0 ->
-  (forall n : NZ, 0 <= n -> A n -> A (S n)) ->
-  (forall n : NZ, n <= 0 -> A n -> A (P n)) ->
-    forall n : NZ, A n.
-Proof (induction_ord_n 0).
-
-Theorem NZlt_ind : forall (n : Z),
-  A (S n) ->
-  (forall m : Z, n < m -> A m -> A (S m)) ->
-   forall m : Z, n < m -> A m.
-Proof.
-intros n H1 H2 m H3.
-apply right_induction with (S n). assumption.
-intros; apply H2; try assumption. now apply <- lt_n_m_succ.
-now apply -> lt_n_m_succ.
-Qed.
-
-Theorem NZle_ind : forall (n : Z),
-  A n ->
-  (forall m : Z, n <= m -> A m -> A (S m)) ->
-   forall m : Z, n <= m -> A m.
-Proof.
-intros n H1 H2 m H3.
-now apply right_induction with n.
-Qed.
-
-End Induction.
-
-Ltac induct_ord n :=
-  try intros until n;
-  pattern n; apply induction_ord; clear n;
-  [unfold NumPrelude.predicate_wd;
-  let n := fresh "n" in
-  let m := fresh "m" in
-  let H := fresh "H" in intros n m H; qmorphism n m | | |].
-
-End ZOrderProperties.
-
-
-
-(*
- Local Variables:
- tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
- End:
-*)