Update before joining all signatures into one.

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

14 files changed, 509 insertions, 387 deletions

diff --git a/theories/Numbers/Integer/Axioms/ZAxioms.v b/theories/Numbers/Integer/Axioms/ZAxioms.v
deleted file mode 100644
index 6527bd11c..000000000
--- a/theories/Numbers/Integer/Axioms/ZAxioms.v
+++ /dev/null
@@ -1,119 +0,0 @@
-Require Export ZDomain.
-
-Module Type IntSignature.
-Declare Module Export ZDomainModule : ZDomainSignature.
-Open Local Scope IntScope.
-
-Parameter Inline O : Z.
-Parameter Inline S : Z -> Z.
-Parameter Inline P : Z -> Z.
-
-Notation "0" := O : IntScope.
-
-Add Morphism S with signature E ==> E as S_wd.
-Add Morphism P with signature E ==> E as P_wd.
-
-Axiom S_inj : forall x y : Z, S x == S y -> x == y.
-Axiom S_P : forall x : Z, S (P x) == x.
-
-Axiom 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.
-
-End IntSignature.
-
-Module IntProperties (Import IntModule : IntSignature).
-Module Export ZDomainPropertiesModule := ZDomainProperties ZDomainModule.
-Open Local Scope IntScope.
-
-Ltac induct n :=
-  try intros until n;
-  pattern n; apply induction; clear n;
-  [unfold NumPrelude.pred_wd;
-  let n := fresh "n" in
-  let m := fresh "m" in
-  let H := fresh "H" in intros n m H; qmorphism n m | | |].
-
-Theorem P_inj : forall x y, P x == P y -> x == y.
-Proof.
-intros x y H.
-setoid_replace x with (S (P x)); [| symmetry; apply S_P].
-setoid_replace y with (S (P y)); [| symmetry; apply S_P].
-now rewrite H.
-Qed.
-
-Theorem P_S : forall x, P (S x) == x.
-Proof.
-intro x.
-apply S_inj.
-now rewrite S_P.
-Qed.
-
-(* The following tactics are intended for replacing a certain
-occurrence of a term t in the goal by (S (P t)) or by (P (S t)).
-Unfortunately, this cannot be done by setoid_replace tactic for two
-reasons. First, it seems impossible to do rewriting when one side of
-the equation in question (S_P or P_S) is a variable, due to bug 1604.
-This does not work even when the predicate is an identifier (e.g.,
-when one tries to rewrite (Q x) into (Q (S (P x)))). Second, the
-setoid_rewrite tactic, like the ordinary rewrite tactic, does not
-allow specifying the exact occurrence of the term to be rewritten. Now
-while not in the setoid context, this occurrence can be specified
-using the pattern tactic, it does not work with setoids, since pattern
-creates a lambda abstractuion, and setoid_rewrite does not work with
-them. *)
-
-Ltac rewrite_SP t set_tac repl thm :=
-let x := fresh "x" in
-set_tac x t;
-setoid_replace x with (repl x); [| symmetry; apply thm];
-unfold x; clear x.
-
-Tactic Notation "rewrite_S_P" constr(t) :=
-rewrite_SP t ltac:(fun x t => (set (x := t))) (fun x => (S (P x))) S_P.
-
-Tactic Notation "rewrite_S_P" constr(t) "at" integer(k) :=
-rewrite_SP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (S (P x))) S_P.
-
-Tactic Notation "rewrite_P_S" constr(t) :=
-rewrite_SP t ltac:(fun x t => (set (x := t))) (fun x => (P (S x))) P_S.
-
-Tactic Notation "rewrite_P_S" constr(t) "at" integer(k) :=
-rewrite_SP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (P (S x))) P_S.
-
-(* One can add tactic notations for replacements in assumptions rather
-than in the goal. For the reason of many possible variants, the core
-of the tactic is factored out. *)
-
-Section Induction.
-
-Variable Q : Z -> Prop.
-Hypothesis Q_wd : pred_wd E Q.
-
-Add Morphism Q with signature E ==> iff as Q_morph.
-Proof Q_wd.
-
-Theorem induction_n :
-  forall n, Q n ->
-    (forall m, Q m -> Q (S m)) ->
-    (forall m, Q m -> Q (P m)) -> forall m, Q m.
-Proof.
-induct n.
-intros; now apply induction.
-intros n IH H1 H2 H3; apply IH; try assumption. apply H3 in H1; now rewrite P_S in H1.
-intros n IH H1 H2 H3; apply IH; try assumption. apply H2 in H1; now rewrite S_P in H1.
-Qed.
-
-End Induction.
-
-Ltac induct_n k n :=
-  try intros until k;
-  pattern k; apply induction_n with (n := n); clear k;
-  [unfold NumPrelude.pred_wd;
-  let n := fresh "n" in
-  let m := fresh "m" in
-  let H := fresh "H" in intros n m H; qmorphism n m | | |].
-
-End IntProperties.
diff --git a/theories/Numbers/Integer/Axioms/ZBase.v b/theories/Numbers/Integer/Axioms/ZBase.v
new file mode 100644
index 000000000..e0b753d4e
--- /dev/null
+++ b/theories/Numbers/Integer/Axioms/ZBase.v
@@ -0,0 +1,103 @@
+Require Export NumPrelude.
+Require Import NZBase.
+
+Module Type ZBaseSig.
+
+Parameter Z : Set.
+Parameter ZE : Z -> Z -> Prop.
+
+Delimit Scope IntScope with Int.
+Bind Scope IntScope with Z.
+Open Local Scope IntScope.
+
+Notation "x == y"  := (ZE x y) (at level 70) : IntScope.
+Notation "x ~= y" := (~ ZE x y) (at level 70) : IntScope.
+
+Axiom ZE_equiv : equiv Z ZE.
+
+Add Relation Z ZE
+ reflexivity proved by (proj1 ZE_equiv)
+ symmetry proved by (proj2 (proj2 ZE_equiv))
+ transitivity proved by (proj1 (proj2 ZE_equiv))
+as ZE_rel.
+
+Parameter Z0 : Z.
+Parameter Zsucc : Z -> Z.
+
+Add Morphism Zsucc with signature ZE ==> ZE as Zsucc_wd.
+
+Notation "0" := Z0 : IntScope.
+Notation "'S'" := Zsucc : IntScope.
+Notation "1" := (S 0) : IntScope.
+(* Note: if we put the line declaring 1 before the line declaring 'S' and
+change (S 0) to (Zsucc 0), then 1 will be parsed but not printed ((S 0)
+will be printed instead of 1) *)
+
+Axiom Zsucc_inj : forall x y : Z, S x == S y -> x == y.
+
+Axiom Zinduction :
+  forall A : predicate Z, predicate_wd ZE A ->
+    A 0 -> (forall x, A x <-> A (S x)) -> forall x, A x.
+
+End ZBaseSig.
+
+Module ZBasePropFunct (Import ZBaseMod : ZBaseSig).
+Open Local Scope IntScope.
+
+Module NZBaseMod <: NZBaseSig.
+
+Definition NZ := Z.
+Definition NZE := ZE.
+Definition NZ0 := Z0.
+Definition NZsucc := Zsucc.
+
+(* Axioms *)
+Definition NZE_equiv := ZE_equiv.
+
+Add Relation NZ NZE
+ 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 NZsucc with signature NZE ==> NZE as NZsucc_wd.
+Proof Zsucc_wd.
+
+Definition NZsucc_inj := Zsucc_inj.
+Definition NZinduction := Zinduction.
+
+End NZBaseMod.
+
+Module Export NZBasePropMod := NZBasePropFunct NZBaseMod.
+
+Theorem Zneq_symm : forall n m : Z, n ~= m -> m ~= n.
+Proof NZneq_symm.
+
+Theorem Zcentral_induction :
+  forall A : Z -> Prop, predicate_wd ZE A ->
+    forall z : Z, A z ->
+      (forall n : Z, A n <-> A (S n)) ->
+        forall n : Z, A n.
+Proof NZcentral_induction.
+
+Theorem Zsucc_inj_wd : forall n m, S n == S m <-> n == m.
+Proof NZsucc_inj_wd.
+
+Theorem Zsucc_inj_neg : forall n m, S n ~= S m <-> n ~= m.
+Proof NZsucc_inj_wd_neg.
+
+Tactic Notation "Zinduct" ident(n) :=
+  induction_maker n ltac:(apply Zinduction).
+(* FIXME: Zinduction probably has to be redeclared in the functor because
+the parameters like Zsucc are not unfolded for Zinduction in the signature *)
+
+Tactic Notation "Zinduct" ident(n) constr(z) :=
+  induction_maker n ltac:(apply Zcentral_induction with z).
+
+End ZBasePropFunct.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Axioms/ZDec.v b/theories/Numbers/Integer/Axioms/ZDec.v
new file mode 100644
index 000000000..9a7aaa099
--- /dev/null
+++ b/theories/Numbers/Integer/Axioms/ZDec.v
@@ -0,0 +1,8 @@
+Axiom E_equiv_e : forall x y : Z, E x y <-> e x y.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Axioms/ZDomain.v b/theories/Numbers/Integer/Axioms/ZDomain.v
index 579f8face..028128cf7 100644
--- a/theories/Numbers/Integer/Axioms/ZDomain.v
+++ b/theories/Numbers/Integer/Axioms/ZDomain.v
@@ -53,3 +53,10 @@ Declare Left Step ZE_stepl.
 Declare Right Step (proj1 (proj2 E_equiv)).
 
 End ZDomainProperties.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Axioms/ZOrder.v b/theories/Numbers/Integer/Axioms/ZOrder.v
index 19a66aea3..cc834b442 100644
--- a/theories/Numbers/Integer/Axioms/ZOrder.v
+++ b/theories/Numbers/Integer/Axioms/ZOrder.v
@@ -1,7 +1,7 @@
 Require Export ZAxioms.
 
 Module Type ZOrderSignature.
-Declare Module Export IntModule : IntSignature.
+Declare Module Export ZBaseMod : ZBaseSig.
 Open Local Scope IntScope.
 
 Parameter Inline lt : Z -> Z -> bool.
@@ -14,13 +14,13 @@ Notation "n <= m" := (le n m) : IntScope.
 
 Axiom le_lt : forall n m, n <= m <-> n < m \/ n == m.
 Axiom lt_irr : forall n, ~ (n < n).
-Axiom lt_S : forall n m, n < (S m) <-> n <= m.
+Axiom lt_succ : forall n m, n < (S m) <-> n <= m.
 
 End ZOrderSignature.
 
 
 Module ZOrderProperties (Import ZOrderModule : ZOrderSignature).
-Module Export IntPropertiesModule := IntProperties IntModule.
+Module Export ZBasePropFunctModule := ZBasePropFunct ZBaseMod.
 Open Local Scope IntScope.
 
 Ltac Zle_intro1 := rewrite le_lt; left.
@@ -32,147 +32,147 @@ Proof.
 intro n; now Zle_intro2.
 Qed.
 
-Theorem lt_n_Sn : forall n, n < S n.
+Theorem lt_n_succn : forall n, n < S n.
 Proof.
-intro n. rewrite lt_S. now Zle_intro2.
+intro n. rewrite lt_succ. now Zle_intro2.
 Qed.
 
-Theorem le_n_Sn : forall n, n <= S n.
+Theorem le_n_succn : forall n, n <= S n.
 Proof.
-intro; Zle_intro1; apply lt_n_Sn.
+intro; Zle_intro1; apply lt_n_succn.
 Qed.
 
-Theorem lt_Pn_n : forall n, P n < n.
+Theorem lt_predn_n : forall n, P n < n.
 Proof.
-intro n; rewrite_S_P n at 2; apply lt_n_Sn.
+intro n; rewrite_succ_pred n at 2; apply lt_n_succn.
 Qed.
 
-Theorem le_Pn_n : forall n, P n <= n.
+Theorem le_predn_n : forall n, P n <= n.
 Proof.
-intro; Zle_intro1; apply lt_Pn_n.
+intro; Zle_intro1; apply lt_predn_n.
 Qed.
 
-Theorem lt_n_Sm : forall n m, n < m -> n < S m.
+Theorem lt_n_succm : forall n m, n < m -> n < S m.
 Proof.
-intros. rewrite lt_S. now Zle_intro1.
+intros. rewrite lt_succ. now Zle_intro1.
 Qed.
 
-Theorem le_n_Sm : forall n m, n <= m -> n <= S m.
+Theorem le_n_succm : forall n m, n <= m -> n <= S m.
 Proof.
-intros n m H; rewrite <- lt_S in H; now Zle_intro1.
+intros n m H; rewrite <- lt_succ in H; now Zle_intro1.
 Qed.
 
-Theorem lt_n_m_P : forall n m, n < m <-> n <= P m.
+Theorem lt_n_m_pred : forall n m, n < m <-> n <= P m.
 Proof.
-intros n m; rewrite_S_P m; rewrite P_S; apply lt_S.
+intros n m; rewrite_succ_pred m; rewrite pred_succ; apply lt_succ.
 Qed.
 
-Theorem not_le_n_Pn : forall n, ~ n <= P n.
+Theorem not_le_n_predn : forall n, ~ n <= P n.
 Proof.
 intros n H; Zle_elim H.
-apply lt_n_Sm in H; rewrite S_P in H; false_hyp H lt_irr.
-pose proof (lt_Pn_n n) as H1; rewrite <- H in H1; false_hyp H1 lt_irr.
+apply lt_n_succm in H; rewrite succ_pred in H; false_hyp H lt_irr.
+pose proof (lt_predn_n n) as H1; rewrite <- H in H1; false_hyp H1 lt_irr.
 Qed.
 
-Theorem le_S : forall n m, n <= S m <-> n <= m \/ n == S m.
+Theorem le_succ : forall n m, n <= S m <-> n <= m \/ n == S m.
 Proof.
-intros n m; rewrite le_lt. now rewrite lt_S.
+intros n m; rewrite le_lt. now rewrite lt_succ.
 Qed.
 
-Theorem lt_P : forall n m, (P n) < m <-> n <= m.
+Theorem lt_pred : forall n m, (P n) < m <-> n <= m.
 Proof.
 intro n; induct_n m (P n).
-split; intro H. false_hyp H lt_irr. false_hyp H not_le_n_Pn.
+split; intro H. false_hyp H lt_irr. false_hyp H not_le_n_predn.
 intros m IH; split; intro H.
-apply -> lt_S in H; Zle_elim H.
-apply -> IH in H; now apply le_n_Sm.
-rewrite <- H; rewrite S_P; now Zle_intro2.
-apply -> le_S in H; destruct H as [H | H].
-apply <- IH in H. now apply lt_n_Sm. rewrite H; rewrite P_S; apply lt_n_Sn.
+apply -> lt_succ in H; Zle_elim H.
+apply -> IH in H; now apply le_n_succm.
+rewrite <- H; rewrite succ_pred; now Zle_intro2.
+apply -> le_succ in H; destruct H as [H | H].
+apply <- IH in H. now apply lt_n_succm. rewrite H; rewrite pred_succ; apply lt_n_succn.
 intros m IH; split; intro H.
-pose proof H as H1. apply lt_n_Sm in H; rewrite S_P in H.
-apply -> IH in H; Zle_elim H. now apply -> lt_n_m_P.
+pose proof H as H1. apply lt_n_succm in H; rewrite succ_pred in H.
+apply -> IH in H; Zle_elim H. now apply -> lt_n_m_pred.
 rewrite H in H1; false_hyp H1 lt_irr.
-pose proof H as H1. apply le_n_Sm in H. rewrite S_P in H.
-apply <- IH in H. apply -> lt_n_m_P in H. Zle_elim H.
-assumption. apply P_inj in H; rewrite H in H1; false_hyp H1 not_le_n_Pn.
+pose proof H as H1. apply le_n_succm in H. rewrite succ_pred in H.
+apply <- IH in H. apply -> lt_n_m_pred in H. Zle_elim H.
+assumption. apply pred_inj in H; rewrite H in H1; false_hyp H1 not_le_n_predn.
 Qed.
 
-Theorem lt_Pn_m : forall n m, n < m -> P n < m.
+Theorem lt_predn_m : forall n m, n < m -> P n < m.
 Proof.
-intros; rewrite lt_P; now Zle_intro1.
+intros; rewrite lt_pred; now Zle_intro1.
 Qed.
 
-Theorem le_Pn_m : forall n m, n <= m -> P n <= m.
+Theorem le_predn_m : forall n m, n <= m -> P n <= m.
 Proof.
-intros n m H; rewrite <- lt_P in H; now Zle_intro1.
+intros n m H; rewrite <- lt_pred in H; now Zle_intro1.
 Qed.
 
-Theorem lt_n_m_S : forall n m, n < m <-> S n <= m.
+Theorem lt_n_m_succ : forall n m, n < m <-> S n <= m.
 Proof.
-intros n m; rewrite_P_S n; rewrite S_P; apply lt_P.
+intros n m; rewrite_pred_succ n; rewrite succ_pred; apply lt_pred.
 Qed.
 
-Theorem lt_Sn_m : forall n m, S n < m -> n < m.
+Theorem lt_succn_m : forall n m, S n < m -> n < m.
 Proof.
-intros n m H; rewrite_P_S n; now apply lt_Pn_m.
+intros n m H; rewrite_pred_succ n; now apply lt_predn_m.
 Qed.
 
-Theorem le_Sn_m : forall n m, S n <= m -> n <= m.
+Theorem le_succn_m : forall n m, S n <= m -> n <= m.
 Proof.
-intros n m H; rewrite <- lt_n_m_S in H; now Zle_intro1.
+intros n m H; rewrite <- lt_n_m_succ in H; now Zle_intro1.
 Qed.
 
-Theorem lt_n_Pm : forall n m, n < P m -> n < m.
+Theorem lt_n_predm : forall n m, n < P m -> n < m.
 Proof.
-intros n m H; rewrite_S_P m; now apply lt_n_Sm.
+intros n m H; rewrite_succ_pred m; now apply lt_n_succm.
 Qed.
 
-Theorem le_n_Pm : forall n m, n <= P m -> n <= m.
+Theorem le_n_predm : forall n m, n <= P m -> n <= m.
 Proof.
-intros n m H; rewrite <- lt_n_m_P in H; now Zle_intro1.
+intros n m H; rewrite <- lt_n_m_pred in H; now Zle_intro1.
 Qed.
 
-Theorem lt_respects_S : forall n m, n < m <-> S n < S m.
+Theorem lt_respects_succ : forall n m, n < m <-> S n < S m.
 Proof.
-intros n m. rewrite lt_n_m_S. symmetry. apply lt_S.
+intros n m. rewrite lt_n_m_succ. symmetry. apply lt_succ.
 Qed.
 
-Theorem le_respects_S : forall n m, n <= m <-> S n <= S m.
+Theorem le_respects_succ : forall n m, n <= m <-> S n <= S m.
 Proof.
 intros n m. do 2 rewrite le_lt.
-firstorder using lt_respects_S S_wd S_inj.
+firstorder using lt_respects_succ succ_wd succ_inj.
 Qed.
 
-Theorem lt_respects_P : forall n m, n < m <-> P n < P m.
+Theorem lt_respects_pred : forall n m, n < m <-> P n < P m.
 Proof.
-intros n m. rewrite lt_n_m_P. symmetry; apply lt_P.
+intros n m. rewrite lt_n_m_pred. symmetry; apply lt_pred.
 Qed.
 
-Theorem le_respects_P : forall n m, n <= m <-> P n <= P m.
+Theorem le_respects_pred : forall n m, n <= m <-> P n <= P m.
 Proof.
 intros n m. do 2 rewrite le_lt.
-firstorder using lt_respects_P P_wd P_inj.
+firstorder using lt_respects_pred pred_wd pred_inj.
 Qed.
 
-Theorem lt_S_P : forall n m, S n < m <-> n < P m.
+Theorem lt_succ_pred : forall n m, S n < m <-> n < P m.
 Proof.
-intros n m; rewrite_P_S n at 2; apply lt_respects_P.
+intros n m; rewrite_pred_succ n at 2; apply lt_respects_pred.
 Qed.
 
-Theorem le_S_P : forall n m, S n <= m <-> n <= P m.
+Theorem le_succ_pred : forall n m, S n <= m <-> n <= P m.
 Proof.
-intros n m; rewrite_P_S n at 2; apply le_respects_P.
+intros n m; rewrite_pred_succ n at 2; apply le_respects_pred.
 Qed.
 
-Theorem lt_P_S : forall n m, P n < m <-> n < S m.
+Theorem lt_pred_succ : forall n m, P n < m <-> n < S m.
 Proof.
-intros n m; rewrite_S_P n at 2; apply lt_respects_S.
+intros n m; rewrite_succ_pred n at 2; apply lt_respects_succ.
 Qed.
 
-Theorem le_P_S : forall n m, P n <= m <-> n <= S m.
+Theorem le_pred_succ : forall n m, P n <= m <-> n <= S m.
 Proof.
-intros n m; rewrite_S_P n at 2; apply le_respects_S.
+intros n m; rewrite_succ_pred n at 2; apply le_respects_succ.
 Qed.
 
 Theorem lt_neq : forall n m, n < m -> n # m.
@@ -184,12 +184,12 @@ Theorem lt_trans : forall n m p, n < m -> m < p -> n < p.
 Proof.
 intros n m; induct_n n m.
 intros p H _; false_hyp H lt_irr.
-intros n IH p H1 H2. apply lt_Sn_m in H1. pose proof (IH p H1 H2) as H3.
-rewrite lt_n_m_S in H3; Zle_elim H3.
-assumption. rewrite <- H3 in H2. rewrite lt_S in H2; Zle_elim H2.
+intros n IH p H1 H2. apply lt_succn_m in H1. pose proof (IH p H1 H2) as H3.
+rewrite lt_n_m_succ in H3; Zle_elim H3.
+assumption. rewrite <- H3 in H2. rewrite lt_succ in H2; Zle_elim H2.
 elimtype False; apply lt_irr with (n := n); now apply IH.
 rewrite H2 in H1; false_hyp H1 lt_irr.
-intros n IH p H1 H2. apply lt_Pn_m. rewrite lt_P in H1; Zle_elim H1.
+intros n IH p H1 H2. apply lt_predn_m. rewrite lt_pred in H1; Zle_elim H1.
 now apply IH. now rewrite H1.
 Qed.
 
@@ -224,15 +224,15 @@ elimtype False; apply lt_irr with (n := n); now apply lt_trans with (m := m).
 now symmetry. assumption. assumption.
 Qed.
 
-Theorem not_lt_Sn_n : forall n, ~ S n < n.
+Theorem not_lt_succn_n : forall n, ~ S n < n.
 Proof.
-intros n H; apply (lt_asymm n (S n)). apply lt_n_Sn. assumption.
+intros n H; apply (lt_asymm n (S n)). apply lt_n_succn. assumption.
 Qed.
 
-Theorem not_le_Sn_n : forall n, ~ S n <= n.
+Theorem not_le_succn_n : forall n, ~ S n <= n.
 Proof.
-intros n H; Zle_elim H. false_hyp H not_lt_Sn_n.
-pose proof (lt_n_Sn n) as H1. rewrite H in H1; false_hyp H1 lt_irr.
+intros n H; Zle_elim H. false_hyp H not_lt_succn_n.
+pose proof (lt_n_succn n) as H1. rewrite H in H1; false_hyp H1 lt_irr.
 Qed.
 
 Theorem lt_gt : forall n m, n < m -> m < n -> False.
@@ -245,13 +245,13 @@ Proof.
 intros n m; induct_n n m.
 right; now left.
 intros n IH; destruct IH as [H | [H | H]].
-rewrite lt_n_m_S in H. rewrite le_lt in H; tauto.
-right; right; rewrite H; apply lt_n_Sn.
-right; right; now apply lt_n_Sm.
+rewrite lt_n_m_succ in H. rewrite le_lt in H; tauto.
+right; right; rewrite H; apply lt_n_succn.
+right; right; now apply lt_n_succm.
 intros n IH; destruct IH as [H | [H | H]].
-left; now apply lt_Pn_m.
-left; rewrite H; apply lt_Pn_n.
-rewrite lt_n_m_P in H. rewrite le_lt in H.
+left; now apply lt_predn_m.
+left; rewrite H; apply lt_predn_n.
+rewrite lt_n_m_pred in H. rewrite le_lt in H.
 setoid_replace (m == P n) with (P n == m) in H using relation iff. tauto.
 split; intro; now symmetry.
 Qed.
@@ -274,7 +274,7 @@ Qed.
 
 Theorem lt_discrete : forall n m, n < m -> m < S n -> False.
 Proof.
-intros n m H1 H2; apply -> lt_S in H2; apply -> lt_ge in H1; false_hyp H2 H1.
+intros n m H1 H2; apply -> lt_succ in H2; apply -> lt_ge in H1; false_hyp H2 H1.
 Qed.
 
 (* Decidability of order can be proved either from totality or from the fact
@@ -283,46 +283,46 @@ that < and <= are boolean functions *)
 (** A corollary of having an order is that Z is infinite in both
 directions *)
 
-Theorem neq_Sn_n : forall n, S n # n.
+Theorem neq_succn_n : forall n, S n # n.
 Proof.
-intros n H. pose proof (lt_n_Sn n) as H1. rewrite H in H1. false_hyp H1 lt_irr.
+intros n H. pose proof (lt_n_succn n) as H1. rewrite H in H1. false_hyp H1 lt_irr.
 Qed.
 
-Theorem neq_Pn_n : forall n, P n # n.
+Theorem neq_predn_n : forall n, P n # n.
 Proof.
-intros n H. apply S_wd in H. rewrite S_P in H. now apply neq_Sn_n with (n := n).
+intros n H. apply succ_wd in H. rewrite succ_pred in H. now apply neq_succn_n with (n := n).
 Qed.
 
-Definition nth_S (n : nat) (m : Z) :=
+Definition nth_succ (n : nat) (m : Z) :=
   nat_rec (fun _ => Z) m (fun _ l => S l) n.
-Definition nth_P (n : nat) (m : Z) :=
+Definition nth_pred (n : nat) (m : Z) :=
   nat_rec (fun _ => Z) m (fun _ l => P l) n.
 
-Lemma lt_m_Skm :
-  forall (n : nat) (m : Z), m < nth_S (Datatypes.S n) m.
+Lemma lt_m_succkm :
+  forall (n : nat) (m : Z), m < nth_succ (Datatypes.S n) m.
 Proof.
 intros n m; induction n as [| n IH]; simpl in *.
-apply lt_n_Sn. now apply lt_n_Sm.
+apply lt_n_succn. now apply lt_n_succm.
 Qed.
 
-Lemma lt_Pkm_m :
-  forall (n : nat) (m : Z), nth_P (Datatypes.S n) m < m.
+Lemma lt_predkm_m :
+  forall (n : nat) (m : Z), nth_pred (Datatypes.S n) m < m.
 Proof.
 intros n m; induction n as [| n IH]; simpl in *.
-apply lt_Pn_n. now apply lt_Pn_m.
+apply lt_predn_n. now apply lt_predn_m.
 Qed.
 
-Theorem neq_m_Skm :
-  forall (n : nat) (m : Z), nth_S (Datatypes.S n) m # m.
+Theorem neq_m_succkm :
+  forall (n : nat) (m : Z), nth_succ (Datatypes.S n) m # m.
 Proof.
-intros n m H. pose proof (lt_m_Skm n m) as H1. rewrite H in H1.
+intros n m H. pose proof (lt_m_succkm n m) as H1. rewrite H in H1.
 false_hyp H1 lt_irr.
 Qed.
 
-Theorem neq_Pkm_m :
-  forall (n : nat) (m : Z), nth_P (Datatypes.S n) m # m.
+Theorem neq_predkm_m :
+  forall (n : nat) (m : Z), nth_pred (Datatypes.S n) m # m.
 Proof.
-intros n m H. pose proof (lt_Pkm_m n m) as H1. rewrite H in H1.
+intros n m H. pose proof (lt_predkm_m n m) as H1. rewrite H in H1.
 false_hyp H1 lt_irr.
 Qed.
 
@@ -331,19 +331,19 @@ in the induction step *)
 
 Section Induction.
 
-Variable Q : Z -> Prop.
-Hypothesis Q_wd : pred_wd E Q.
+Variable A : Z -> Prop.
+Hypothesis Q_wd : predicate_wd E A.
 
-Add Morphism Q with signature E ==> iff as Q_morph.
+Add Morphism A with signature E ==> iff as Q_morph.
 Proof Q_wd.
 
 Section Center.
 
-Variable z : Z. (* Q z is the basis of induction *)
+Variable z : Z. (* A z is the basis of induction *)
 
 Section RightInduction.
 
-Let Q' := fun n : Z => forall m, z <= m -> m < n -> Q m.
+Let Q' := fun n : Z => forall m, z <= m -> m < n -> A m.
 
 Add Morphism Q' with signature E ==> iff as Q'_pos_wd.
 Proof.
@@ -351,26 +351,26 @@ intros x1 x2 H; unfold Q'; qmorphism x1 x2.
 Qed.
 
 Theorem right_induction :
-  Q z -> (forall n, z <= n -> Q n -> Q (S n)) -> forall n, z <= n -> Q n.
+  A z -> (forall n, z <= n -> A n -> A (S n)) -> forall n, z <= n -> A n.
 Proof.
 intros Qz QS k k_ge_z.
 assert (H : forall n, 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 lt_S in H3; Zle_elim H3. now apply IH.
-Zle_elim H2. rewrite_S_P m.
-apply QS. now apply -> lt_n_m_P. apply IH. now apply -> lt_n_m_P.
-rewrite H3; apply lt_Pn_n. now rewrite <- H2.
-intros n IH m H2 H3. apply IH. assumption. now apply lt_n_Pm.
+rewrite lt_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 lt_predn_n. 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 lt_n_Sn.
+apply k_ge_z. apply lt_n_succn.
 Qed.
 
 End RightInduction.
 
 Section LeftInduction.
 
-Let Q' := fun n : Z => forall m, m <= z -> n < m -> Q m.
+Let Q' := fun n : Z => forall m, m <= z -> n < m -> A m.
 
 Add Morphism Q' with signature E ==> iff as Q'_neg_wd.
 Proof.
@@ -378,28 +378,28 @@ intros x1 x2 H; unfold Q'; qmorphism x1 x2.
 Qed.
 
 Theorem left_induction :
-  Q z -> (forall n, n <= z -> Q n -> Q (P n)) -> forall n, n <= z -> Q n.
+  A z -> (forall n, n <= z -> A n -> A (P n)) -> forall n, n <= z -> A n.
 Proof.
 intros Qz QP k k_le_z.
 assert (H : forall n, 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_Sn_m.
+intros n IH m H2 H3. apply IH. assumption. now apply lt_succn_m.
 intros n IH m H2 H3.
-rewrite lt_P in H3; Zle_elim H3. now apply IH.
-Zle_elim H2. rewrite_P_S m.
-apply QP. now apply -> lt_n_m_S. apply IH. now apply -> lt_n_m_S.
-rewrite H3; apply lt_n_Sn. now rewrite H2.
+rewrite lt_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 lt_n_succn. now rewrite H2.
 pose proof (H (P k)) as H1; unfold Q' in H1. apply H1.
-apply k_le_z. apply lt_Pn_n.
+apply k_le_z. apply lt_predn_n.
 Qed.
 
 End LeftInduction.
 
 Theorem induction_ord_n :
-  Q z ->
-  (forall n, z <= n -> Q n -> Q (S n)) ->
-  (forall n, n <= z -> Q n -> Q (P n)) ->
-    forall n, Q n.
+  A z ->
+  (forall n, z <= n -> A n -> A (S n)) ->
+  (forall n, n <= z -> A n -> A (P n)) ->
+    forall n, A n.
 Proof.
 intros Qz QS QP n.
 destruct (lt_total n z) as [H | [H | H]].
@@ -411,27 +411,27 @@ Qed.
 End Center.
 
 Theorem induction_ord :
-  Q 0 ->
-  (forall n, 0 <= n -> Q n -> Q (S n)) ->
-  (forall n, n <= 0 -> Q n -> Q (P n)) ->
-    forall n, Q n.
+  A 0 ->
+  (forall n, 0 <= n -> A n -> A (S n)) ->
+  (forall n, n <= 0 -> A n -> A (P n)) ->
+    forall n, A n.
 Proof (induction_ord_n 0).
 
 Theorem lt_ind : forall (n : Z),
-  Q (S n) ->
-  (forall m : Z, n < m -> Q m -> Q (S m)) ->
-   forall m : Z, n < m -> Q m.
+  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_S.
-now apply -> lt_n_m_S.
+intros; apply H2; try assumption. now apply <- lt_n_m_succ.
+now apply -> lt_n_m_succ.
 Qed.
 
 Theorem le_ind : forall (n : Z),
-  Q n ->
-  (forall m : Z, n <= m -> Q m -> Q (S m)) ->
-   forall m : Z, n <= m -> Q m.
+  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.
@@ -442,10 +442,17 @@ End Induction.
 Ltac induct_ord n :=
   try intros until n;
   pattern n; apply induction_ord; clear n;
-  [unfold NumPrelude.pred_wd;
+  [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:
+*)
diff --git a/theories/Numbers/Integer/Axioms/ZPlus.v b/theories/Numbers/Integer/Axioms/ZPlus.v
index 6c1f49231..624f85f04 100644
--- a/theories/Numbers/Integer/Axioms/ZPlus.v
+++ b/theories/Numbers/Integer/Axioms/ZPlus.v
@@ -1,7 +1,7 @@
 Require Export ZAxioms.
 
 Module Type ZPlusSignature.
-Declare Module Export IntModule : IntSignature.
+Declare Module Export ZBaseMod : ZBaseSig.
 Open Local Scope IntScope.
 
 Parameter Inline plus : Z -> Z -> Z.
@@ -17,62 +17,62 @@ Add Morphism minus with signature E ==> E ==> E as minus_wd.
 Add Morphism uminus with signature E ==> E as uminus_wd.
 
 Axiom plus_0 : forall n, 0 + n == n.
-Axiom plus_S : forall n m, (S n) + m == S (n + m).
+Axiom plus_succ : forall n m, (S n) + m == S (n + m).
 
 Axiom minus_0 : forall n, n - 0 == n.
-Axiom minus_S : forall n m, n - (S m) == P (n - m).
+Axiom minus_succ : forall n m, n - (S m) == P (n - m).
 
 Axiom uminus_0 : - 0 == 0.
-Axiom uminus_S : forall n, - (S n) == P (- n).
+Axiom uminus_succ : forall n, - (S n) == P (- n).
 
 End ZPlusSignature.
 
 Module ZPlusProperties (Import ZPlusModule : ZPlusSignature).
-Module Export IntPropertiesModule := IntProperties IntModule.
+Module Export ZBasePropFunctModule := ZBasePropFunct ZBaseMod.
 Open Local Scope IntScope.
 
-Theorem plus_P : forall n m, P n + m == P (n + m).
+Theorem plus_pred : forall n m, P n + m == P (n + m).
 Proof.
-intros n m. rewrite_S_P n at 2. rewrite plus_S. now rewrite P_S.
+intros n m. rewrite_succ_pred n at 2. rewrite plus_succ. now rewrite pred_succ.
 Qed.
 
-Theorem minus_P : forall n m, n - (P m) == S (n - m).
+Theorem minus_pred : forall n m, n - (P m) == S (n - m).
 Proof.
-intros n m. rewrite_S_P m at 2. rewrite minus_S. now rewrite S_P.
+intros n m. rewrite_succ_pred m at 2. rewrite minus_succ. now rewrite succ_pred.
 Qed.
 
-Theorem uminus_P : forall n, - (P n) == S (- n).
+Theorem uminus_pred : forall n, - (P n) == S (- n).
 Proof.
-intro n. rewrite_S_P n at 2. rewrite uminus_S. now rewrite S_P.
+intro n. rewrite_succ_pred n at 2. rewrite uminus_succ. now rewrite succ_pred.
 Qed.
 
 Theorem plus_n_0 : forall n, n + 0 == n.
 Proof.
 induct n.
 now rewrite plus_0.
-intros n IH. rewrite plus_S. now rewrite IH.
-intros n IH. rewrite plus_P. now rewrite IH.
+intros n IH. rewrite plus_succ. now rewrite IH.
+intros n IH. rewrite plus_pred. now rewrite IH.
 Qed.
 
-Theorem plus_n_Sm : forall n m, n + S m == S (n + m).
+Theorem plus_n_succm : forall n m, n + S m == S (n + m).
 Proof.
 intros n m; induct n.
 now do 2 rewrite plus_0.
-intros n IH. do 2 rewrite plus_S. now rewrite IH.
-intros n IH. do 2 rewrite plus_P. rewrite IH. rewrite P_S; now rewrite S_P.
+intros n IH. do 2 rewrite plus_succ. now rewrite IH.
+intros n IH. do 2 rewrite plus_pred. rewrite IH. rewrite pred_succ; now rewrite succ_pred.
 Qed.
 
-Theorem plus_n_Pm : forall n m, n + P m == P (n + m).
+Theorem plus_n_predm : forall n m, n + P m == P (n + m).
 Proof.
-intros n m; rewrite_S_P m at 2. rewrite plus_n_Sm; now rewrite P_S.
+intros n m; rewrite_succ_pred m at 2. rewrite plus_n_succm; now rewrite pred_succ.
 Qed.
 
 Theorem plus_opp_minus : forall n m, n + (- m) == n - m.
 Proof.
 induct m.
 rewrite uminus_0; rewrite minus_0; now rewrite plus_n_0.
-intros m IH. rewrite uminus_S; rewrite minus_S. rewrite plus_n_Pm; now rewrite IH.
-intros m IH. rewrite uminus_P; rewrite minus_P. rewrite plus_n_Sm; now rewrite IH.
+intros m IH. rewrite uminus_succ; rewrite minus_succ. rewrite plus_n_predm; now rewrite IH.
+intros m IH. rewrite uminus_pred; rewrite minus_pred. rewrite plus_n_succm; now rewrite IH.
 Qed.
 
 Theorem minus_0_n : forall n, 0 - n == - n.
@@ -80,38 +80,38 @@ Proof.
 intro n; rewrite <- plus_opp_minus; now rewrite plus_0.
 Qed.
 
-Theorem minus_Sn_m : forall n m, S n - m == S (n - m).
+Theorem minus_succn_m : forall n m, S n - m == S (n - m).
 Proof.
-intros n m; do 2 rewrite <- plus_opp_minus; now rewrite plus_S.
+intros n m; do 2 rewrite <- plus_opp_minus; now rewrite plus_succ.
 Qed.
 
-Theorem minus_Pn_m : forall n m, P n - m == P (n - m).
+Theorem minus_predn_m : forall n m, P n - m == P (n - m).
 Proof.
-intros n m. rewrite_S_P n at 2; rewrite minus_Sn_m; now rewrite P_S.
+intros n m. rewrite_succ_pred n at 2; rewrite minus_succn_m; now rewrite pred_succ.
 Qed.
 
 Theorem plus_assoc : forall n m p, n + (m + p) == (n + m) + p.
 Proof.
 intros n m p; induct n.
 now do 2 rewrite plus_0.
-intros n IH. do 3 rewrite plus_S. now rewrite IH.
-intros n IH. do 3 rewrite plus_P. now rewrite IH.
+intros n IH. do 3 rewrite plus_succ. now rewrite IH.
+intros n IH. do 3 rewrite plus_pred. now rewrite IH.
 Qed.
 
 Theorem plus_comm : forall n m, n + m == m + n.
 Proof.
 intros n m; induct n.
 rewrite plus_0; now rewrite plus_n_0.
-intros n IH; rewrite plus_S; rewrite plus_n_Sm; now rewrite IH.
-intros n IH; rewrite plus_P; rewrite plus_n_Pm; now rewrite IH.
+intros n IH; rewrite plus_succ; rewrite plus_n_succm; now rewrite IH.
+intros n IH; rewrite plus_pred; rewrite plus_n_predm; now rewrite IH.
 Qed.
 
 Theorem minus_diag : forall n, n - n == 0.
 Proof.
 induct n.
 now rewrite minus_0.
-intros n IH. rewrite minus_S; rewrite minus_Sn_m; rewrite P_S; now rewrite IH.
-intros n IH. rewrite minus_P; rewrite minus_Pn_m; rewrite S_P; now rewrite IH.
+intros n IH. rewrite minus_succ; rewrite minus_succn_m; rewrite pred_succ; now rewrite IH.
+intros n IH. rewrite minus_pred; rewrite minus_predn_m; rewrite succ_pred; now rewrite IH.
 Qed.
 
 Theorem plus_opp_r : forall n, n + (- n) == 0.
@@ -144,16 +144,16 @@ Theorem double_opp : forall n, - (- n) == n.
 Proof.
 induct n.
 now do 2 rewrite uminus_0.
-intros n IH. rewrite uminus_S; rewrite uminus_P; now rewrite IH.
-intros n IH. rewrite uminus_P; rewrite uminus_S; now rewrite IH.
+intros n IH. rewrite uminus_succ; rewrite uminus_pred; now rewrite IH.
+intros n IH. rewrite uminus_pred; rewrite uminus_succ; now rewrite IH.
 Qed.
 
 Theorem opp_plus_distr : forall n m, - (n + m) == - n + (- m).
 Proof.
 intros n m; induct n.
 rewrite uminus_0; now do 2 rewrite plus_0.
-intros n IH. rewrite plus_S; do 2 rewrite uminus_S. rewrite IH. now rewrite plus_P.
-intros n IH. rewrite plus_P; do 2 rewrite uminus_P. rewrite IH. now rewrite plus_S.
+intros n IH. rewrite plus_succ; do 2 rewrite uminus_succ. rewrite IH. now rewrite plus_pred.
+intros n IH. rewrite plus_pred; do 2 rewrite uminus_pred. rewrite IH. now rewrite plus_succ.
 Qed.
 
 Theorem opp_minus_distr : forall n m, - (n - m) == - n + m.
@@ -219,3 +219,10 @@ intros n m H. rewrite <- (plus_minus_inverse m n). rewrite H. apply plus_n_0.
 Qed.
 
 End ZPlusProperties.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Axioms/ZPlusOrder.v b/theories/Numbers/Integer/Axioms/ZPlusOrder.v
index 946bdf3cb..95f0fa8c6 100644
--- a/theories/Numbers/Integer/Axioms/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Axioms/ZPlusOrder.v
@@ -3,7 +3,7 @@ Require Export ZPlus.
 
 Module ZPlusOrderProperties (Import ZPlusModule : ZPlusSignature)
                             (Import ZOrderModule : ZOrderSignature with
-                              Module IntModule := ZPlusModule.IntModule).
+                              Module ZBaseMod := ZPlusModule.ZBaseMod).
 Module Export ZPlusPropertiesModule := ZPlusProperties ZPlusModule.
 Module Export ZOrderPropertiesModule := ZOrderProperties ZOrderModule.
 (* <W> Grammar extension: in [tactic:simple_tactic], some rule has been masked !!! *)
@@ -13,8 +13,8 @@ Theorem plus_lt_compat_l : forall n m p, n < m <-> p + n < p + m.
 Proof.
 intros n m p; induct p.
 now do 2 rewrite plus_0.
-intros p IH. do 2 rewrite plus_S. now rewrite <- lt_respects_S.
-intros p IH. do 2 rewrite plus_P. now rewrite <- lt_respects_P.
+intros p IH. do 2 rewrite plus_succ. now rewrite <- lt_respects_succ.
+intros p IH. do 2 rewrite plus_pred. now rewrite <- lt_respects_pred.
 Qed.
 
 Theorem plus_lt_compat_r : forall n m p, n < m <-> n + p < m + p.
@@ -25,7 +25,7 @@ Qed.
 
 Theorem plus_le_compat_l : forall n m p, n <= m <-> p + n <= p + m.
 Proof.
-intros n m p; do 2 rewrite <- lt_S. rewrite <- plus_n_Sm;
+intros n m p; do 2 rewrite <- lt_succ. rewrite <- plus_n_succm;
 apply plus_lt_compat_l.
 Qed.
 
@@ -69,14 +69,14 @@ Proof.
 induct n.
 induct_ord m.
 intro H; false_hyp H lt_irr.
-intros m H1 IH H2. rewrite uminus_S. rewrite uminus_0 in *.
-Zle_elim H1. apply IH in H1. now apply lt_Pn_m.
-rewrite <- H1; rewrite uminus_0; apply lt_Pn_n.
-intros m H1 IH H2. apply lt_n_Pm in H2. apply -> le_gt in H1. false_hyp H2 H1.
-intros n IH m H. rewrite uminus_S.
-apply -> lt_S_P in H. apply IH in H. rewrite uminus_P in H. now apply -> lt_S_P.
-intros n IH m H. rewrite uminus_P.
-apply -> lt_P_S in H. apply IH in H. rewrite uminus_S in H. now apply -> lt_P_S.
+intros m H1 IH H2. rewrite uminus_succ. rewrite uminus_0 in *.
+Zle_elim H1. apply IH in H1. now apply lt_predn_m.
+rewrite <- H1; rewrite uminus_0; apply lt_predn_n.
+intros m H1 IH H2. apply lt_n_predm in H2. apply -> le_gt in H1. false_hyp H2 H1.
+intros n IH m H. rewrite uminus_succ.
+apply -> lt_succ_pred in H. apply IH in H. rewrite uminus_pred in H. now apply -> lt_succ_pred.
+intros n IH m H. rewrite uminus_pred.
+apply -> lt_pred_succ in H. apply IH in H. rewrite uminus_succ in H. now apply -> lt_pred_succ.
 Qed.
 
 Theorem lt_opp : forall n m, n < m <-> - m < - n.
@@ -158,3 +158,10 @@ rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0.
 Qed.
 
 End ZPlusOrderProperties.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Axioms/ZPred.v b/theories/Numbers/Integer/Axioms/ZPred.v
new file mode 100644
index 000000000..ffcb2dea8
--- /dev/null
+++ b/theories/Numbers/Integer/Axioms/ZPred.v
@@ -0,0 +1,60 @@
+Axiom succ_pred : forall x : Z, S (P x) == x.
+Add Morphism P with signature E ==> E as pred_wd.
+
+Theorem pred_inj : forall x y, P x == P y -> x == y.
+Proof.
+intros x y H.
+setoid_replace x with (S (P x)); [| symmetry; apply succ_pred].
+setoid_replace y with (S (P y)); [| symmetry; apply succ_pred].
+now rewrite H.
+Qed.
+
+Theorem pred_succ : forall x, P (S x) == x.
+Proof.
+intro x.
+apply succ_inj.
+now rewrite succ_pred.
+Qed.
+
+(* The following tactics are intended for replacing a certain
+occurrence of a term t in the goal by (S (P t)) or by (P (S t)).
+Unfortunately, this cannot be done by setoid_replace tactic for two
+reasons. First, it seems impossible to do rewriting when one side of
+the equation in question (succ_pred or pred_succ) is a variable, due to bug 1604.
+This does not work even when the predicate is an identifier (e.g.,
+when one tries to rewrite (A x) into (A (S (P x)))). Second, the
+setoid_rewrite tactic, like the ordinary rewrite tactic, does not
+allow specifying the exact occurrence of the term to be rewritten. Now
+while not in the setoid context, this occurrence can be specified
+using the pattern tactic, it does not work with setoids, since pattern
+creates a lambda abstractuion, and setoid_rewrite does not work with
+them. *)
+
+Ltac rewrite_succP t set_tac repl thm :=
+let x := fresh "x" in
+set_tac x t;
+setoid_replace x with (repl x); [| symmetry; apply thm];
+unfold x; clear x.
+
+Tactic Notation "rewrite_succ_pred" constr(t) :=
+rewrite_succP t ltac:(fun x t => (set (x := t))) (fun x => (S (P x))) succ_pred.
+
+Tactic Notation "rewrite_succ_pred" constr(t) "at" integer(k) :=
+rewrite_succP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (S (P x))) succ_pred.
+
+Tactic Notation "rewrite_pred_succ" constr(t) :=
+rewrite_succP t ltac:(fun x t => (set (x := t))) (fun x => (P (S x))) pred_succ.
+
+Tactic Notation "rewrite_pred_succ" constr(t) "at" integer(k) :=
+rewrite_succP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (P (S x))) pred_succ.
+
+(* One can add tactic notations for replacements in assumptions rather
+than in the goal. For the reason of many possible variants, the core
+of the tactic is factored out. *)
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Axioms/ZTimes.v b/theories/Numbers/Integer/Axioms/ZTimes.v
index 5dc0b7505..38311aa2b 100644
--- a/theories/Numbers/Integer/Axioms/ZTimes.v
+++ b/theories/Numbers/Integer/Axioms/ZTimes.v
@@ -11,7 +11,7 @@ Notation "x * y" := (times x y) : IntScope.
 Add Morphism times with signature E ==> E ==> E as times_wd.
 
 Axiom times_0 : forall n, n * 0 == 0.
-Axiom times_S : forall n m, n * (S m) == n * m + n.
+Axiom times_succ : forall n m, n * (S m) == n * m + n.
 
 End ZTimesSignature.
 
@@ -19,9 +19,9 @@ Module ZTimesProperties (Import ZTimesModule : ZTimesSignature).
 Module Export ZPlusPropertiesModule := ZPlusProperties ZPlusModule.
 Open Local Scope IntScope.
 
-Theorem times_P : forall n m, n * (P m) == n * m - n.
+Theorem times_pred : forall n m, n * (P m) == n * m - n.
 Proof.
-intros n m. rewrite_S_P m at 2. rewrite times_S. rewrite <- plus_minus_distr.
+intros n m. rewrite_succ_pred m at 2. rewrite times_succ. rewrite <- plus_minus_distr.
 rewrite minus_diag. now rewrite plus_n_0.
 Qed.
 
@@ -29,26 +29,26 @@ Theorem times_0_n : forall n, 0 * n == 0.
 Proof.
 induct n.
 now rewrite times_0.
-intros n IH. rewrite times_S. rewrite IH; now rewrite plus_0.
-intros n IH. rewrite times_P. rewrite IH; now rewrite minus_0.
+intros n IH. rewrite times_succ. rewrite IH; now rewrite plus_0.
+intros n IH. rewrite times_pred. rewrite IH; now rewrite minus_0.
 Qed.
 
-Theorem times_Sn_m : forall n m, (S n) * m == n * m + m.
+Theorem times_succn_m : forall n m, (S n) * m == n * m + m.
 Proof.
 induct m.
 do 2 rewrite times_0. now rewrite plus_0.
-intros m IH. do 2 rewrite times_S. rewrite IH.
+intros m IH. do 2 rewrite times_succ. rewrite IH.
 do 2 rewrite <- plus_assoc. apply plus_wd. reflexivity.
-do 2 rewrite plus_n_Sm; now rewrite plus_comm.
-intros m IH. do 2 rewrite times_P. rewrite IH.
+do 2 rewrite plus_n_succm; now rewrite plus_comm.
+intros m IH. do 2 rewrite times_pred. rewrite IH.
 rewrite <- plus_minus_swap. do 2 rewrite <- plus_minus_distr.
 apply plus_wd. reflexivity.
-rewrite minus_S. now rewrite minus_Pn_m.
+rewrite minus_succ. now rewrite minus_predn_m.
 Qed.
 
-Theorem times_Pn_m : forall n m, (P n) * m == n * m - m.
+Theorem times_predn_m : forall n m, (P n) * m == n * m - m.
 Proof.
-intros n m. rewrite_S_P n at 2. rewrite times_Sn_m.
+intros n m. rewrite_succ_pred n at 2. rewrite times_succn_m.
 rewrite <- plus_minus_distr. rewrite minus_diag; now rewrite plus_n_0.
 Qed.
 
@@ -56,17 +56,17 @@ Theorem times_comm : forall n m, n * m == m * n.
 Proof.
 intros n m; induct n.
 rewrite times_0_n; now rewrite times_0.
-intros n IH. rewrite times_Sn_m; rewrite times_S; now rewrite IH.
-intros n IH. rewrite times_Pn_m; rewrite times_P; now rewrite IH.
+intros n IH. rewrite times_succn_m; rewrite times_succ; now rewrite IH.
+intros n IH. rewrite times_predn_m; rewrite times_pred; now rewrite IH.
 Qed.
 
 Theorem times_opp_r : forall n m, n * (- m) == - (n * m).
 Proof.
 intros n m; induct m.
 rewrite uminus_0; rewrite times_0; now rewrite uminus_0.
-intros m IH. rewrite uminus_S. rewrite times_P; rewrite times_S. rewrite IH.
+intros m IH. rewrite uminus_succ. rewrite times_pred; rewrite times_succ. rewrite IH.
 rewrite <- plus_opp_minus; now rewrite opp_plus_distr.
-intros m IH. rewrite uminus_P. rewrite times_P; rewrite times_S. rewrite IH.
+intros m IH. rewrite uminus_pred. rewrite times_pred; rewrite times_succ. rewrite IH.
 now rewrite opp_minus_distr.
 Qed.
 
@@ -85,9 +85,9 @@ Theorem times_plus_distr_r : forall n m p, n * (m + p) == n * m + n * p.
 Proof.
 intros n m p; induct m.
 rewrite times_0; now do 2 rewrite plus_0.
-intros m IH. rewrite plus_S. do 2 rewrite times_S. rewrite IH.
+intros m IH. rewrite plus_succ. do 2 rewrite times_succ. rewrite IH.
 do 2 rewrite <- plus_assoc; apply plus_wd; [reflexivity | apply plus_comm].
-intros m IH. rewrite plus_P. do 2 rewrite times_P. rewrite IH.
+intros m IH. rewrite plus_pred. do 2 rewrite times_pred. rewrite IH.
 apply plus_minus_swap.
 Qed.
 
@@ -113,8 +113,15 @@ Theorem times_assoc : forall n m p, n * (m * p) == (n * m) * p.
 Proof.
 intros n m p; induct p.
 now do 3 rewrite times_0.
-intros p IH. do 2 rewrite times_S. rewrite times_plus_distr_r. now rewrite IH.
-intros p IH. do 2 rewrite times_P. rewrite times_minus_distr_r. now rewrite IH.
+intros p IH. do 2 rewrite times_succ. rewrite times_plus_distr_r. now rewrite IH.
+intros p IH. do 2 rewrite times_pred. rewrite times_minus_distr_r. now rewrite IH.
 Qed.
 
 End ZTimesProperties.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Axioms/ZTimesOrder.v b/theories/Numbers/Integer/Axioms/ZTimesOrder.v
index 28c07a99d..055342bcc 100644
--- a/theories/Numbers/Integer/Axioms/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Axioms/ZTimesOrder.v
@@ -3,7 +3,7 @@ Require Export ZPlusOrder.
 
 Module ZTimesOrderProperties (Import ZTimesModule : ZTimesSignature)
                              (Import ZOrderModule : ZOrderSignature with
-                               Module IntModule := ZTimesModule.ZPlusModule.IntModule).
+                               Module ZBaseMod := ZTimesModule.ZPlusModule.ZBaseMod).
 Module Export ZTimesPropertiesModule := ZTimesProperties ZTimesModule.
 Module Export ZPlusOrderPropertiesModule :=
   ZPlusOrderProperties ZTimesModule.ZPlusModule ZOrderModule.
@@ -13,11 +13,11 @@ Theorem mult_lt_compat_r : forall n m p, 0 < p -> n < m -> n * p < m * p.
 Proof.
 intros n m p; induct_ord p.
 intros H _; false_hyp H lt_irr.
-intros p H IH H1 H2. do 2 rewrite times_S.
-apply -> lt_S in H1; Zle_elim H1.
+intros p H IH H1 H2. do 2 rewrite times_succ.
+apply -> lt_succ in H1; Zle_elim H1.
 apply plus_lt_compat. now apply IH. assumption.
 rewrite <- H1. do 2 rewrite times_0; now do 2 rewrite plus_0.
-intros p H IH H1 H2. apply lt_n_Pm in H1. apply -> le_gt in H.
+intros p H IH H1 H2. apply lt_n_predm in H1. apply -> le_gt in H.
 false_hyp H1 H.
 Qed.
 
@@ -87,3 +87,10 @@ apply neq_symm. apply lt_neq. now apply mult_pos_pos.
 Qed.
 
 End ZTimesOrderProperties.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
index 683b86ec6..73b0bee7e 100644
--- a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
+++ b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
@@ -1,17 +1,17 @@
 Require Import NPlus.
 Require Export ZAxioms.
 
-Module NatPairsDomain (Import NPlusModule : NPlusSignature) <: ZDomainSignature.
+Module NatPairsDomain (Import NPlusMod : NPlusSig) <: ZDomainSignature.
 (*  with Definition Z :=
-    (NPM.NatModule.DomainModule.N * NPM.NatModule.DomainModule.N)%type
+    (NPM.NBaseMod.DomainModule.N * NPM.NBaseMod.DomainModule.N)%type
   with Definition E :=
     fun p1 p2  =>
-      NPM.NatModule.DomainModule.E (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1))
+      NPM.NBaseMod.DomainModule.E (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1))
   with Definition e :=
     fun p1 p2  =>
-      NPM.NatModule.DomainModule.e (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1)).*)
+      NPM.NBaseMod.DomainModule.e (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1)).*)
 
-Module Export NPlusPropertiesModule := NPlusProperties NatModule NPlusModule.
+Module Export NPlusPropMod := NPlusPropFunct NBaseMod NPlusMod.
 Open Local Scope NatScope.
 
 Definition Z : Set := (N * N)%type.
@@ -68,14 +68,14 @@ Qed.
 
 End NatPairsDomain.
 
-Module NatPairsInt (Import NPlusModule : NPlusSignature) <: IntSignature.
-Module Export ZDomainModule := NatPairsDomain NPlusModule.
+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) := (NatModule.S (fst n), snd n).
-Definition P (n : Z) := (fst n, NatModule.S (snd n)).
+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
@@ -84,47 +84,47 @@ 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 S_wd.
+Add Morphism S with signature E ==> E as succ_wd.
 Proof.
 unfold S, E; intros n m H; simpl.
-do 2 rewrite plus_S_l; now rewrite H.
+do 2 rewrite plus_succ_l; now rewrite H.
 Qed.
 
-Add Morphism P with signature E ==> E as P_wd.
+Add Morphism P with signature E ==> E as pred_wd.
 Proof.
 unfold P, E; intros n m H; simpl.
-do 2 rewrite plus_S_r; now rewrite H.
+do 2 rewrite plus_succ_r; now rewrite H.
 Qed.
 
-Theorem S_inj : forall x y : Z, S x == S y -> x == y.
+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_S_l in H. now apply S_inj in H.
+do 2 rewrite plus_succ_l in H. now apply succ_inj in H.
 Qed.
 
-Theorem S_P : forall x : Z, S (P x) == x.
+Theorem succ_pred : forall x : Z, S (P x) == x.
 Proof.
 intro x; unfold S, P, E; simpl.
-rewrite plus_S_l; now rewrite plus_S_r.
+rewrite plus_succ_l; now rewrite plus_succ_r.
 Qed.
 
 Section Induction.
 Open Scope NatScope. (* automatically closes at the end of the section *)
-Variable Q : Z -> Prop.
-Hypothesis Q_wd : pred_wd E Q.
+Variable A : Z -> Prop.
+Hypothesis Q_wd : predicate_wd E A.
 
-Add Morphism Q with signature E ==> iff as Q_morph.
+Add Morphism A with signature E ==> iff as Q_morph.
 Proof.
 exact Q_wd.
 Qed.
 
 Theorem induction :
-  Q 0 -> (forall x, Q x -> Q (S x)) -> (forall x, Q x -> Q (P x)) -> forall x, Q x.
+  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, pred_wd, E in *.
+intros Q0 QS QP x; unfold O, S, P, predicate_wd, E in *.
 destruct x as [n m].
-cut (forall p : N, Q (p, 0)); [intro H1 |].
-cut (forall p : N, Q (0, p)); [intro H2 |].
+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.
@@ -139,3 +139,10 @@ Qed.
 End Induction.
 
 End NatPairsInt.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsOrder.v b/theories/Numbers/Integer/NatPairs/ZPairsOrder.v
index 29181e0c6..8943afde9 100644
--- a/theories/Numbers/Integer/NatPairs/ZPairsOrder.v
+++ b/theories/Numbers/Integer/NatPairs/ZPairsOrder.v
@@ -2,12 +2,12 @@ Require Import NPlusOrder.
 Require Export ZPlusOrder.
 Require Export ZPairsPlus.
 
-Module NatPairsOrder (Import NPlusModule : NPlusSignature)
-                     (Import NOrderModule : NOrderSignature
-                        with Module NatModule := NPlusModule.NatModule) <: ZOrderSignature.
+Module NatPairsOrder (Import NPlusMod : NPlusSig)
+                     (Import NOrderModule : NOrderSig
+                        with Module NBaseMod := NPlusMod.NBaseMod) <: ZOrderSignature.
 Module Import NPlusOrderPropertiesModule :=
-  NPlusOrderProperties NPlusModule NOrderModule.
-Module Export IntModule := NatPairsInt NPlusModule.
+  NPlusOrderProperties NPlusMod NOrderModule.
+Module Export ZBaseMod := NatPairsInt NPlusMod.
 Open Local Scope NatScope.
 
 Definition lt (p1 p2 : Z) := (fst p1) + (snd p2) < (fst p2) + (snd p1).
@@ -58,17 +58,17 @@ unfold le, E; intros x1 y1 H1 x2 y2 H2; simpl.
 rewrite eq_true_iff. do 2 rewrite le_lt.
 pose proof (lt_wd x1 y1 H1 x2 y2 H2) as H; unfold lt in H; rewrite H; clear H.
 (* This is a remark about an extra level of definitions created by
-"with Module NatModule := NPlusModule.NatModule" constraint in the beginning
+"with Module NBaseMod := NPlusMod.NBaseMod" constraint in the beginning
 of this functor. We cannot just say "fold (x1 == x2)%Int" because it turns out
-that it expand to (NPlusModule.NatModule.NDomainModule.E ... ...), since
-NPlusModule was imported first. On the other hand, the goal uses
-NOrderModule.NatModule.NDomainModule.E, or just NDomainModule.E, since le_lt
+that it expand to (NPlusMod.NBaseMod.NDomainModule.E ... ...), since
+NPlusMod was imported first. On the other hand, the goal uses
+NOrderModule.NBaseMod.NDomainModule.E, or just NDomainModule.E, since le_lt
 theorem was proved in NOrderDomain module. (E without qualifiers refers to
 ZDomainModule.E.) Therefore, we issue the "replace" command. It would be nicer,
-though, if the constraint "with Module NatModule := NPlusModule.NatModule" in the
+though, if the constraint "with Module NBaseMod := NPlusMod.NBaseMod" in the
 declaration of this functor would not create an extra level of definitions
 and there would be only one NDomainModule.E. *)
-replace NDomainModule.E with NPlusModule.NatModule.NDomainModule.E by reflexivity.
+replace NDomainModule.E with NPlusMod.NBaseMod.NDomainModule.E by reflexivity.
 fold (x1 == x2)%Int. fold (y1 == y2)%Int.
 assert (H1' : (x1 == y1)%Int); [exact H1 |].
 (* We do this instead of "fold (x1 == y1)%Int in H1" *)
@@ -86,26 +86,33 @@ Qed.
 Theorem lt_irr : forall n : Z, ~ (n < n).
 Proof.
 intros n; unfold lt, E; simpl. apply lt_irr.
-(* refers to NPlusOrderPropertiesModule.NOrderPropertiesModule.lt_irr *)
+(* refers to NPlusOrderPropertiesModule.NOrderPropFunctModule.lt_irr *)
 Qed.
 
-Theorem lt_S : forall n m, n < (S m) <-> n <= m.
+Theorem lt_succ : forall n m, n < (S m) <-> n <= m.
 Proof.
-intros n m; unfold lt, le, E; simpl. rewrite plus_S_l; apply lt_S.
+intros n m; unfold lt, le, E; simpl. rewrite plus_succ_l; apply lt_succ.
 Qed.
 
 End NatPairsOrder.
 
 (* Since to define the order on integers we need both plus and order
 on natural numbers, we can export the properties of plus and order together *)
-(*Module NatPairsPlusOrderProperties (NPlusModule : NPlusSignature)
-                                   (NOrderModule : NOrderSignature
-                                     with Module NatModule := NPlusModule.NatModule).
-Module Export NatPairsPlusModule := NatPairsPlus NPlusModule.
-Module Export NatPairsOrderModule := NatPairsOrder NPlusModule NOrderModule.
+(*Module NatPairsPlusOrderProperties (NPlusMod : NPlusSig)
+                                   (NOrderModule : NOrderSig
+                                     with Module NBaseMod := NPlusMod.NBaseMod).
+Module Export NatPairsPlusModule := NatPairsPlus NPlusMod.
+Module Export NatPairsOrderModule := NatPairsOrder NPlusMod NOrderModule.
 Module Export NatPairsPlusOrderPropertiesModule :=
   ZPlusOrderProperties NatPairsPlusModule NatPairsOrderModule.
 End NatPairsPlusOrderProperties.*)
-(* We cannot prove to Coq that NatPairsPlusModule.IntModule and
-NatPairsOrderModule.IntModule are the same *)
+(* We cannot prove to Coq that NatPairsPlusModule.ZBaseMod and
+NatPairsOrderModule.ZBaseMod are the same *)
 
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
index d18076265..d1ae7679b 100644
--- a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
+++ b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
@@ -2,8 +2,8 @@ Require Import NPlus.
 Require Export ZPlus.
 Require Export ZPairsAxioms.
 
-Module NatPairsPlus (Import NPlusModule : NPlusSignature) <: ZPlusSignature.
-Module Export IntModule := NatPairsInt NPlusModule.
+Module NatPairsPlus (Import NPlusMod : NPlusSig) <: ZPlusSignature.
+Module Export ZBaseMod := NatPairsInt NPlusMod.
 Open Local Scope NatScope.
 
 Definition plus (x y : Z) := ((fst x) + (fst y), (snd x) + (snd y)).
@@ -31,7 +31,7 @@ Add Morphism minus with signature E ==> E ==> E as minus_wd.
 Proof.
 unfold E, plus; intros x1 y1 H1 x2 y2 H2; simpl.
 rewrite plus_comm in H2. symmetry in H2; rewrite plus_comm in H2.
-pose proof (NPlusModule.plus_wd (fst x1 + snd y1) (fst y1 + snd x1) H1
+pose proof (NPlusMod.plus_wd (fst x1 + snd y1) (fst y1 + snd x1) H1
                                 (snd x2 + fst y2) (snd y2 + fst x2) H2) as H.
 rewrite plus_shuffle1. symmetry. now rewrite plus_shuffle1.
 Qed.
@@ -46,12 +46,12 @@ Open Local Scope IntScope.
 
 Theorem plus_0 : forall n, 0 + n == n.
 Proof.
-intro n; unfold plus, E; simpl. now do 2 rewrite NPlusModule.plus_0_l.
+intro n; unfold plus, E; simpl. now do 2 rewrite NPlusMod.plus_0_l.
 Qed.
 
-Theorem plus_S : forall n m, (S n) + m == S (n + m).
+Theorem plus_succ : forall n m, (S n) + m == S (n + m).
 Proof.
-intros n m; unfold plus, E; simpl. now do 2 rewrite NPlusModule.plus_S_l.
+intros n m; unfold plus, E; simpl. now do 2 rewrite NPlusMod.plus_succ_l.
 Qed.
 
 Theorem minus_0 : forall n, n - 0 == n.
@@ -59,9 +59,9 @@ Proof.
 intro n; unfold minus, E; simpl. now do 2 rewrite plus_0_r.
 Qed.
 
-Theorem minus_S : forall n m, n - (S m) == P (n - m).
+Theorem minus_succ : forall n m, n - (S m) == P (n - m).
 Proof.
-intros n m; unfold minus, E; simpl. symmetry; now rewrite plus_S_r.
+intros n m; unfold minus, E; simpl. symmetry; now rewrite plus_succ_r.
 Qed.
 
 Theorem uminus_0 : - 0 == 0.
@@ -69,14 +69,21 @@ Proof.
 unfold uminus, E; simpl. now rewrite plus_0_l.
 Qed.
 
-Theorem uminus_S : forall n, - (S n) == P (- n).
+Theorem uminus_succ : forall n, - (S n) == P (- n).
 Proof.
 reflexivity.
 Qed.
 
 End NatPairsPlus.
 
-Module NatPairsPlusProperties (NPlusModule : NPlusSignature).
-Module Export NatPairsPlusModule := NatPairsPlus NPlusModule.
+Module NatPairsPlusProperties (NPlusMod : NPlusSig).
+Module Export NatPairsPlusModule := NatPairsPlus NPlusMod.
 Module Export NatPairsPlusPropertiesModule := ZPlusProperties NatPairsPlusModule.
 End NatPairsPlusProperties.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
index b72847c08..47bf8cd08 100644
--- a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
+++ b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
@@ -3,9 +3,9 @@ Require Import NTimes.
 Require Export ZTimes.
 Require Export ZPairsPlus.
 
-Module NatPairsTimes (Import NTimesModule : NTimesSignature) <: ZTimesSignature.
-Module Export ZPlusModule := NatPairsPlus NTimesModule.NPlusModule. (* "NTimesModule." is optional *)
-Module Import NTimesPropertiesModule := NTimesProperties NTimesModule.
+Module NatPairsTimes (Import NTimesMod : NTimesSig) <: ZTimesSignature.
+Module Export ZPlusModule := NatPairsPlus NTimesMod.NPlusMod. (* "NTimesMod." is optional *)
+Module Import NTimesPropertiesModule := NTimesPropFunct NTimesMod.
 Open Local Scope NatScope.
 
 Definition times (n m : Z) :=
@@ -41,15 +41,22 @@ intro n; unfold times, E; simpl.
 repeat rewrite times_0_r. now rewrite plus_assoc.
 Qed.
 
-Theorem times_S : forall n m, n * (S m) == n * m + n.
+Theorem times_succ : forall n m, n * (S m) == n * m + n.
 Proof.
 intros n m; unfold times, S, E; simpl.
-do 2 rewrite times_S_r. ring.
+do 2 rewrite times_succ_r. ring.
 Qed.
 
 End NatPairsTimes.
 
-Module NatPairsTimesProperties (NTimesModule : NTimesSignature).
-Module Export NatPairsTimesModule := NatPairsTimes NTimesModule.
+Module NatPairsTimesProperties (NTimesMod : NTimesSig).
+Module Export NatPairsTimesModule := NatPairsTimes NTimesMod.
 Module Export NatPairsTimesPropertiesModule := ZTimesProperties NatPairsTimesModule.
 End NatPairsTimesProperties.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)