In abstract parts of theories/Numbers, plus/times becomes add/mul,

for increased consistency with bignums parts 

(commit part II: names of files + additional translation minus --> sub)



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

11 files changed, 167 insertions, 167 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZAdd.v
index d72d00379..daa7c530b 100644
--- a/theories/Numbers/Integer/Abstract/ZPlus.v
+++ b/theories/Numbers/Integer/Abstract/ZAdd.v
@@ -12,7 +12,7 @@
 
 Require Export ZBase.
 
-Module ZPlusPropFunct (Import ZAxiomsMod : ZAxiomsSig).
+Module ZAddPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZBasePropMod := ZBasePropFunct ZAxiomsMod.
 Open Local Scope IntScope.
 
@@ -26,11 +26,11 @@ Proof NZadd_0_l.
 Theorem Zadd_succ_l : forall n m : Z, (S n) + m == S (n + m).
 Proof NZadd_succ_l.
 
-Theorem Zminus_0_r : forall n : Z, n - 0 == n.
-Proof NZminus_0_r.
+Theorem Zsub_0_r : forall n : Z, n - 0 == n.
+Proof NZsub_0_r.
 
-Theorem Zminus_succ_r : forall n m : Z, n - (S m) == P (n - m).
-Proof NZminus_succ_r.
+Theorem Zsub_succ_r : forall n m : Z, n - (S m) == P (n - m).
+Proof NZsub_succ_r.
 
 Theorem Zopp_0 : - 0 == 0.
 Proof Zopp_0.
@@ -88,30 +88,30 @@ Qed.
 Theorem Zadd_opp_r : forall n m : Z, n + (- m) == n - m.
 Proof.
 NZinduct m.
-rewrite Zopp_0; rewrite Zminus_0_r; now rewrite Zadd_0_r.
-intro m. rewrite Zopp_succ, Zminus_succ_r, Zadd_pred_r; now rewrite Zpred_inj_wd.
+rewrite Zopp_0; rewrite Zsub_0_r; now rewrite Zadd_0_r.
+intro m. rewrite Zopp_succ, Zsub_succ_r, Zadd_pred_r; now rewrite Zpred_inj_wd.
 Qed.
 
-Theorem Zminus_0_l : forall n : Z, 0 - n == - n.
+Theorem Zsub_0_l : forall n : Z, 0 - n == - n.
 Proof.
 intro n; rewrite <- Zadd_opp_r; now rewrite Zadd_0_l.
 Qed.
 
-Theorem Zminus_succ_l : forall n m : Z, S n - m == S (n - m).
+Theorem Zsub_succ_l : forall n m : Z, S n - m == S (n - m).
 Proof.
 intros n m; do 2 rewrite <- Zadd_opp_r; now rewrite Zadd_succ_l.
 Qed.
 
-Theorem Zminus_pred_l : forall n m : Z, P n - m == P (n - m).
+Theorem Zsub_pred_l : forall n m : Z, P n - m == P (n - m).
 Proof.
 intros n m. rewrite <- (Zsucc_pred n) at 2.
-rewrite Zminus_succ_l; now rewrite Zpred_succ.
+rewrite Zsub_succ_l; now rewrite Zpred_succ.
 Qed.
 
-Theorem Zminus_pred_r : forall n m : Z, n - (P m) == S (n - m).
+Theorem Zsub_pred_r : forall n m : Z, n - (P m) == S (n - m).
 Proof.
 intros n m. rewrite <- (Zsucc_pred m) at 2.
-rewrite Zminus_succ_r; now rewrite Zsucc_pred.
+rewrite Zsub_succ_r; now rewrite Zsucc_pred.
 Qed.
 
 Theorem Zopp_pred : forall n : Z, - (P n) == S (- n).
@@ -120,16 +120,16 @@ intro n. rewrite <- (Zsucc_pred n) at 2.
 rewrite Zopp_succ. now rewrite Zsucc_pred.
 Qed.
 
-Theorem Zminus_diag : forall n : Z, n - n == 0.
+Theorem Zsub_diag : forall n : Z, n - n == 0.
 Proof.
 NZinduct n.
-now rewrite Zminus_0_r.
-intro n. rewrite Zminus_succ_r, Zminus_succ_l; now rewrite Zpred_succ.
+now rewrite Zsub_0_r.
+intro n. rewrite Zsub_succ_r, Zsub_succ_l; now rewrite Zpred_succ.
 Qed.
 
 Theorem Zadd_opp_diag_l : forall n : Z, - n + n == 0.
 Proof.
-intro n; now rewrite Zadd_comm, Zadd_opp_r, Zminus_diag.
+intro n; now rewrite Zadd_comm, Zadd_opp_r, Zsub_diag.
 Qed.
 
 Theorem Zadd_opp_diag_r : forall n : Z, n + (- n) == 0.
@@ -142,7 +142,7 @@ Proof.
 intros n m; rewrite <- Zadd_opp_r; now rewrite Zadd_comm.
 Qed.
 
-Theorem Zadd_minus_assoc : forall n m p : Z, n + (m - p) == (n + m) - p.
+Theorem Zadd_sub_assoc : forall n m p : Z, n + (m - p) == (n + m) - p.
 Proof.
 intros n m p; do 2 rewrite <- Zadd_opp_r; now rewrite Zadd_assoc.
 Qed.
@@ -162,7 +162,7 @@ intro n. rewrite Zadd_succ_l; do 2 rewrite Zopp_succ; rewrite Zadd_pred_l.
 now rewrite Zpred_inj_wd.
 Qed.
 
-Theorem Zopp_minus_distr : forall n m : Z, - (n - m) == - n + m.
+Theorem Zopp_sub_distr : forall n m : Z, - (n - m) == - n + m.
 Proof.
 intros n m; rewrite <- Zadd_opp_r, Zopp_add_distr.
 now rewrite Zopp_involutive.
@@ -188,58 +188,58 @@ Proof.
 symmetry; apply Zeq_opp_l.
 Qed.
 
-Theorem Zminus_add_distr : forall n m p : Z, n - (m + p) == (n - m) - p.
+Theorem Zsub_add_distr : forall n m p : Z, n - (m + p) == (n - m) - p.
 Proof.
 intros n m p; rewrite <- Zadd_opp_r, Zopp_add_distr, Zadd_assoc.
 now do 2 rewrite Zadd_opp_r.
 Qed.
 
-Theorem Zminus_minus_distr : forall n m p : Z, n - (m - p) == (n - m) + p.
+Theorem Zsub_sub_distr : forall n m p : Z, n - (m - p) == (n - m) + p.
 Proof.
-intros n m p; rewrite <- Zadd_opp_r, Zopp_minus_distr, Zadd_assoc.
+intros n m p; rewrite <- Zadd_opp_r, Zopp_sub_distr, Zadd_assoc.
 now rewrite Zadd_opp_r.
 Qed.
 
-Theorem minus_opp_l : forall n m : Z, - n - m == - m - n.
+Theorem sub_opp_l : forall n m : Z, - n - m == - m - n.
 Proof.
 intros n m. do 2 rewrite <- Zadd_opp_r. now rewrite Zadd_comm.
 Qed.
 
-Theorem Zminus_opp_r : forall n m : Z, n - (- m) == n + m.
+Theorem Zsub_opp_r : forall n m : Z, n - (- m) == n + m.
 Proof.
 intros n m; rewrite <- Zadd_opp_r; now rewrite Zopp_involutive.
 Qed.
 
-Theorem Zadd_minus_swap : forall n m p : Z, n + m - p == n - p + m.
+Theorem Zadd_sub_swap : forall n m p : Z, n + m - p == n - p + m.
 Proof.
-intros n m p. rewrite <- Zadd_minus_assoc, <- (Zadd_opp_r n p), <- Zadd_assoc.
+intros n m p. rewrite <- Zadd_sub_assoc, <- (Zadd_opp_r n p), <- Zadd_assoc.
 now rewrite Zadd_opp_l.
 Qed.
 
-Theorem Zminus_cancel_l : forall n m p : Z, n - m == n - p <-> m == p.
+Theorem Zsub_cancel_l : forall n m p : Z, n - m == n - p <-> m == p.
 Proof.
 intros n m p. rewrite <- (Zadd_cancel_l (n - m) (n - p) (- n)).
-do 2 rewrite Zadd_minus_assoc. rewrite Zadd_opp_diag_l; do 2 rewrite Zminus_0_l.
+do 2 rewrite Zadd_sub_assoc. rewrite Zadd_opp_diag_l; do 2 rewrite Zsub_0_l.
 apply Zopp_inj_wd.
 Qed.
 
-Theorem Zminus_cancel_r : forall n m p : Z, n - p == m - p <-> n == m.
+Theorem Zsub_cancel_r : forall n m p : Z, n - p == m - p <-> n == m.
 Proof.
 intros n m p.
 stepl (n - p + p == m - p + p) by apply Zadd_cancel_r.
-now do 2 rewrite <- Zminus_minus_distr, Zminus_diag, Zminus_0_r.
+now do 2 rewrite <- Zsub_sub_distr, Zsub_diag, Zsub_0_r.
 Qed.
 
 (* The next several theorems are devoted to moving terms from one side of
 an equation to the other. The name contains the operation in the original
-equation (add or minus) and the indication whether the left or right term
+equation (add or sub) and the indication whether the left or right term
 is moved. *)
 
 Theorem Zadd_move_l : forall n m p : Z, n + m == p <-> m == p - n.
 Proof.
 intros n m p.
-stepl (n + m - n == p - n) by apply Zminus_cancel_r.
-now rewrite Zadd_comm, <- Zadd_minus_assoc, Zminus_diag, Zadd_0_r.
+stepl (n + m - n == p - n) by apply Zsub_cancel_r.
+now rewrite Zadd_comm, <- Zadd_sub_assoc, Zsub_diag, Zadd_0_r.
 Qed.
 
 Theorem Zadd_move_r : forall n m p : Z, n + m == p <-> n == p - m.
@@ -251,34 +251,34 @@ Qed.
 n - m == p to n == p + m since subtraction is in the right-hand side of
 the equation. Hence the following two theorems. *)
 
-Theorem Zminus_move_l : forall n m p : Z, n - m == p <-> - m == p - n.
+Theorem Zsub_move_l : forall n m p : Z, n - m == p <-> - m == p - n.
 Proof.
 intros n m p; rewrite <- (Zadd_opp_r n m); apply Zadd_move_l.
 Qed.
 
-Theorem Zminus_move_r : forall n m p : Z, n - m == p <-> n == p + m.
+Theorem Zsub_move_r : forall n m p : Z, n - m == p <-> n == p + m.
 Proof.
-intros n m p; rewrite <- (Zadd_opp_r n m). now rewrite Zadd_move_r, Zminus_opp_r.
+intros n m p; rewrite <- (Zadd_opp_r n m). now rewrite Zadd_move_r, Zsub_opp_r.
 Qed.
 
 Theorem Zadd_move_0_l : forall n m : Z, n + m == 0 <-> m == - n.
 Proof.
-intros n m; now rewrite Zadd_move_l, Zminus_0_l.
+intros n m; now rewrite Zadd_move_l, Zsub_0_l.
 Qed.
 
 Theorem Zadd_move_0_r : forall n m : Z, n + m == 0 <-> n == - m.
 Proof.
-intros n m; now rewrite Zadd_move_r, Zminus_0_l.
+intros n m; now rewrite Zadd_move_r, Zsub_0_l.
 Qed.
 
-Theorem Zminus_move_0_l : forall n m : Z, n - m == 0 <-> - m == - n.
+Theorem Zsub_move_0_l : forall n m : Z, n - m == 0 <-> - m == - n.
 Proof.
-intros n m. now rewrite Zminus_move_l, Zminus_0_l.
+intros n m. now rewrite Zsub_move_l, Zsub_0_l.
 Qed.
 
-Theorem Zminus_move_0_r : forall n m : Z, n - m == 0 <-> n == m.
+Theorem Zsub_move_0_r : forall n m : Z, n - m == 0 <-> n == m.
 Proof.
-intros n m. now rewrite Zminus_move_r, Zadd_0_l.
+intros n m. now rewrite Zsub_move_r, Zadd_0_l.
 Qed.
 
 (* The following section is devoted to cancellation of like terms. The name
@@ -286,22 +286,22 @@ includes the first operator and the position of the term being canceled. *)
 
 Theorem Zadd_simpl_l : forall n m : Z, n + m - n == m.
 Proof.
-intros; now rewrite Zadd_minus_swap, Zminus_diag, Zadd_0_l.
+intros; now rewrite Zadd_sub_swap, Zsub_diag, Zadd_0_l.
 Qed.
 
 Theorem Zadd_simpl_r : forall n m : Z, n + m - m == n.
 Proof.
-intros; now rewrite <- Zadd_minus_assoc, Zminus_diag, Zadd_0_r.
+intros; now rewrite <- Zadd_sub_assoc, Zsub_diag, Zadd_0_r.
 Qed.
 
-Theorem Zminus_simpl_l : forall n m : Z, - n - m + n == - m.
+Theorem Zsub_simpl_l : forall n m : Z, - n - m + n == - m.
 Proof.
-intros; now rewrite <- Zadd_minus_swap, Zadd_opp_diag_l, Zminus_0_l.
+intros; now rewrite <- Zadd_sub_swap, Zadd_opp_diag_l, Zsub_0_l.
 Qed.
 
-Theorem Zminus_simpl_r : forall n m : Z, n - m + m == n.
+Theorem Zsub_simpl_r : forall n m : Z, n - m + m == n.
 Proof.
-intros; now rewrite <- Zminus_minus_distr, Zminus_diag, Zminus_0_r.
+intros; now rewrite <- Zsub_sub_distr, Zsub_diag, Zsub_0_r.
 Qed.
 
 (* Now we have two sums or differences; the name includes the two operators
@@ -309,8 +309,8 @@ and the position of the terms being canceled *)
 
 Theorem Zadd_add_simpl_l_l : forall n m p : Z, (n + m) - (n + p) == m - p.
 Proof.
-intros n m p. now rewrite (Zadd_comm n m), <- Zadd_minus_assoc,
-Zminus_add_distr, Zminus_diag, Zminus_0_l, Zadd_opp_r.
+intros n m p. now rewrite (Zadd_comm n m), <- Zadd_sub_assoc,
+Zsub_add_distr, Zsub_diag, Zsub_0_l, Zadd_opp_r.
 Qed.
 
 Theorem Zadd_add_simpl_l_r : forall n m p : Z, (n + m) - (p + n) == m - p.
@@ -328,18 +328,18 @@ Proof.
 intros n m p. rewrite (Zadd_comm p m); apply Zadd_add_simpl_r_l.
 Qed.
 
-Theorem Zminus_add_simpl_r_l : forall n m p : Z, (n - m) + (m + p) == n + p.
+Theorem Zsub_add_simpl_r_l : forall n m p : Z, (n - m) + (m + p) == n + p.
 Proof.
-intros n m p. now rewrite <- Zminus_minus_distr, Zminus_add_distr, Zminus_diag,
-Zminus_0_l, Zminus_opp_r.
+intros n m p. now rewrite <- Zsub_sub_distr, Zsub_add_distr, Zsub_diag,
+Zsub_0_l, Zsub_opp_r.
 Qed.
 
-Theorem Zminus_add_simpl_r_r : forall n m p : Z, (n - m) + (p + m) == n + p.
+Theorem Zsub_add_simpl_r_r : forall n m p : Z, (n - m) + (p + m) == n + p.
 Proof.
-intros n m p. rewrite (Zadd_comm p m); apply Zminus_add_simpl_r_l.
+intros n m p. rewrite (Zadd_comm p m); apply Zsub_add_simpl_r_l.
 Qed.
 
 (* Of course, there are many other variants *)
 
-End ZPlusPropFunct.
+End ZAddPropFunct.
 
diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v
index 85f671498..917e3fc12 100644
--- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -12,7 +12,7 @@
 
 Require Export ZLt.
 
-Module ZPlusOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
+Module ZAddOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZOrderPropMod := ZOrderPropFunct ZAxiomsMod.
 Open Local Scope IntScope.
 
@@ -109,50 +109,50 @@ Proof.
 intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_le_mono.
 Qed.
 
-(** Minus and order *)
+(** Sub and order *)
 
-Theorem Zlt_0_minus : forall n m : Z, 0 < m - n <-> n < m.
+Theorem Zlt_0_sub : forall n m : Z, 0 < m - n <-> n < m.
 Proof.
 intros n m. stepl (0 + n < m - n + n) by symmetry; apply Zadd_lt_mono_r.
-rewrite Zadd_0_l; now rewrite Zminus_simpl_r.
+rewrite Zadd_0_l; now rewrite Zsub_simpl_r.
 Qed.
 
-Notation Zminus_pos := Zlt_0_minus (only parsing).
+Notation Zsub_pos := Zlt_0_sub (only parsing).
 
-Theorem Zle_0_minus : forall n m : Z, 0 <= m - n <-> n <= m.
+Theorem Zle_0_sub : forall n m : Z, 0 <= m - n <-> n <= m.
 Proof.
 intros n m; stepl (0 + n <= m - n + n) by symmetry; apply Zadd_le_mono_r.
-rewrite Zadd_0_l; now rewrite Zminus_simpl_r.
+rewrite Zadd_0_l; now rewrite Zsub_simpl_r.
 Qed.
 
-Notation Zminus_nonneg := Zle_0_minus (only parsing).
+Notation Zsub_nonneg := Zle_0_sub (only parsing).
 
-Theorem Zlt_minus_0 : forall n m : Z, n - m < 0 <-> n < m.
+Theorem Zlt_sub_0 : forall n m : Z, n - m < 0 <-> n < m.
 Proof.
 intros n m. stepl (n - m + m < 0 + m) by symmetry; apply Zadd_lt_mono_r.
-rewrite Zadd_0_l; now rewrite Zminus_simpl_r.
+rewrite Zadd_0_l; now rewrite Zsub_simpl_r.
 Qed.
 
-Notation Zminus_neg := Zlt_minus_0 (only parsing).
+Notation Zsub_neg := Zlt_sub_0 (only parsing).
 
-Theorem Zle_minus_0 : forall n m : Z, n - m <= 0 <-> n <= m.
+Theorem Zle_sub_0 : forall n m : Z, n - m <= 0 <-> n <= m.
 Proof.
 intros n m. stepl (n - m + m <= 0 + m) by symmetry; apply Zadd_le_mono_r.
-rewrite Zadd_0_l; now rewrite Zminus_simpl_r.
+rewrite Zadd_0_l; now rewrite Zsub_simpl_r.
 Qed.
 
-Notation Zminus_nonpos := Zle_minus_0 (only parsing).
+Notation Zsub_nonpos := Zle_sub_0 (only parsing).
 
 Theorem Zopp_lt_mono : forall n m : Z, n < m <-> - m < - n.
 Proof.
 intros n m. stepr (m + - m < m + - n) by symmetry; apply Zadd_lt_mono_l.
-do 2 rewrite Zadd_opp_r. rewrite Zminus_diag. symmetry; apply Zlt_0_minus.
+do 2 rewrite Zadd_opp_r. rewrite Zsub_diag. symmetry; apply Zlt_0_sub.
 Qed.
 
 Theorem Zopp_le_mono : forall n m : Z, n <= m <-> - m <= - n.
 Proof.
 intros n m. stepr (m + - m <= m + - n) by symmetry; apply Zadd_le_mono_l.
-do 2 rewrite Zadd_opp_r. rewrite Zminus_diag. symmetry; apply Zle_0_minus.
+do 2 rewrite Zadd_opp_r. rewrite Zsub_diag. symmetry; apply Zle_0_sub.
 Qed.
 
 Theorem Zopp_pos_neg : forall n : Z, 0 < - n <-> n < 0.
@@ -175,172 +175,172 @@ Proof.
 intro n. rewrite (Zopp_le_mono 0 n). now rewrite Zopp_0.
 Qed.
 
-Theorem Zminus_lt_mono_l : forall n m p : Z, n < m <-> p - m < p - n.
+Theorem Zsub_lt_mono_l : forall n m p : Z, n < m <-> p - m < p - n.
 Proof.
 intros n m p. do 2 rewrite <- Zadd_opp_r. rewrite <- Zadd_lt_mono_l.
 apply Zopp_lt_mono.
 Qed.
 
-Theorem Zminus_lt_mono_r : forall n m p : Z, n < m <-> n - p < m - p.
+Theorem Zsub_lt_mono_r : forall n m p : Z, n < m <-> n - p < m - p.
 Proof.
 intros n m p; do 2 rewrite <- Zadd_opp_r; apply Zadd_lt_mono_r.
 Qed.
 
-Theorem Zminus_lt_mono : forall n m p q : Z, n < m -> q < p -> n - p < m - q.
+Theorem Zsub_lt_mono : forall n m p q : Z, n < m -> q < p -> n - p < m - q.
 Proof.
 intros n m p q H1 H2.
 apply NZlt_trans with (m - p);
-[now apply -> Zminus_lt_mono_r | now apply -> Zminus_lt_mono_l].
+[now apply -> Zsub_lt_mono_r | now apply -> Zsub_lt_mono_l].
 Qed.
 
-Theorem Zminus_le_mono_l : forall n m p : Z, n <= m <-> p - m <= p - n.
+Theorem Zsub_le_mono_l : forall n m p : Z, n <= m <-> p - m <= p - n.
 Proof.
 intros n m p; do 2 rewrite <- Zadd_opp_r; rewrite <- Zadd_le_mono_l;
 apply Zopp_le_mono.
 Qed.
 
-Theorem Zminus_le_mono_r : forall n m p : Z, n <= m <-> n - p <= m - p.
+Theorem Zsub_le_mono_r : forall n m p : Z, n <= m <-> n - p <= m - p.
 Proof.
 intros n m p; do 2 rewrite <- Zadd_opp_r; apply Zadd_le_mono_r.
 Qed.
 
-Theorem Zminus_le_mono : forall n m p q : Z, n <= m -> q <= p -> n - p <= m - q.
+Theorem Zsub_le_mono : forall n m p q : Z, n <= m -> q <= p -> n - p <= m - q.
 Proof.
 intros n m p q H1 H2.
 apply NZle_trans with (m - p);
-[now apply -> Zminus_le_mono_r | now apply -> Zminus_le_mono_l].
+[now apply -> Zsub_le_mono_r | now apply -> Zsub_le_mono_l].
 Qed.
 
-Theorem Zminus_lt_le_mono : forall n m p q : Z, n < m -> q <= p -> n - p < m - q.
+Theorem Zsub_lt_le_mono : forall n m p q : Z, n < m -> q <= p -> n - p < m - q.
 Proof.
 intros n m p q H1 H2.
 apply NZlt_le_trans with (m - p);
-[now apply -> Zminus_lt_mono_r | now apply -> Zminus_le_mono_l].
+[now apply -> Zsub_lt_mono_r | now apply -> Zsub_le_mono_l].
 Qed.
 
-Theorem Zminus_le_lt_mono : forall n m p q : Z, n <= m -> q < p -> n - p < m - q.
+Theorem Zsub_le_lt_mono : forall n m p q : Z, n <= m -> q < p -> n - p < m - q.
 Proof.
 intros n m p q H1 H2.
 apply NZle_lt_trans with (m - p);
-[now apply -> Zminus_le_mono_r | now apply -> Zminus_lt_mono_l].
+[now apply -> Zsub_le_mono_r | now apply -> Zsub_lt_mono_l].
 Qed.
 
-Theorem Zle_lt_minus_lt : forall n m p q : Z, n <= m -> p - n < q - m -> p < q.
+Theorem Zle_lt_sub_lt : forall n m p q : Z, n <= m -> p - n < q - m -> p < q.
 Proof.
 intros n m p q H1 H2. apply (Zle_lt_add_lt (- m) (- n));
 [now apply -> Zopp_le_mono | now do 2 rewrite Zadd_opp_r].
 Qed.
 
-Theorem Zlt_le_minus_lt : forall n m p q : Z, n < m -> p - n <= q - m -> p < q.
+Theorem Zlt_le_sub_lt : forall n m p q : Z, n < m -> p - n <= q - m -> p < q.
 Proof.
 intros n m p q H1 H2. apply (Zlt_le_add_lt (- m) (- n));
 [now apply -> Zopp_lt_mono | now do 2 rewrite Zadd_opp_r].
 Qed.
 
-Theorem Zle_le_minus_lt : forall n m p q : Z, n <= m -> p - n <= q - m -> p <= q.
+Theorem Zle_le_sub_lt : forall n m p q : Z, n <= m -> p - n <= q - m -> p <= q.
 Proof.
 intros n m p q H1 H2. apply (Zle_le_add_le (- m) (- n));
 [now apply -> Zopp_le_mono | now do 2 rewrite Zadd_opp_r].
 Qed.
 
-Theorem Zlt_add_lt_minus_r : forall n m p : Z, n + p < m <-> n < m - p.
+Theorem Zlt_add_lt_sub_r : forall n m p : Z, n + p < m <-> n < m - p.
 Proof.
-intros n m p. stepl (n + p - p < m - p) by symmetry; apply Zminus_lt_mono_r.
+intros n m p. stepl (n + p - p < m - p) by symmetry; apply Zsub_lt_mono_r.
 now rewrite Zadd_simpl_r.
 Qed.
 
-Theorem Zle_add_le_minus_r : forall n m p : Z, n + p <= m <-> n <= m - p.
+Theorem Zle_add_le_sub_r : forall n m p : Z, n + p <= m <-> n <= m - p.
 Proof.
-intros n m p. stepl (n + p - p <= m - p) by symmetry; apply Zminus_le_mono_r.
+intros n m p. stepl (n + p - p <= m - p) by symmetry; apply Zsub_le_mono_r.
 now rewrite Zadd_simpl_r.
 Qed.
 
-Theorem Zlt_add_lt_minus_l : forall n m p : Z, n + p < m <-> p < m - n.
+Theorem Zlt_add_lt_sub_l : forall n m p : Z, n + p < m <-> p < m - n.
 Proof.
-intros n m p. rewrite Zadd_comm; apply Zlt_add_lt_minus_r.
+intros n m p. rewrite Zadd_comm; apply Zlt_add_lt_sub_r.
 Qed.
 
-Theorem Zle_add_le_minus_l : forall n m p : Z, n + p <= m <-> p <= m - n.
+Theorem Zle_add_le_sub_l : forall n m p : Z, n + p <= m <-> p <= m - n.
 Proof.
-intros n m p. rewrite Zadd_comm; apply Zle_add_le_minus_r.
+intros n m p. rewrite Zadd_comm; apply Zle_add_le_sub_r.
 Qed.
 
-Theorem Zlt_minus_lt_add_r : forall n m p : Z, n - p < m <-> n < m + p.
+Theorem Zlt_sub_lt_add_r : forall n m p : Z, n - p < m <-> n < m + p.
 Proof.
 intros n m p. stepl (n - p + p < m + p) by symmetry; apply Zadd_lt_mono_r.
-now rewrite Zminus_simpl_r.
+now rewrite Zsub_simpl_r.
 Qed.
 
-Theorem Zle_minus_le_add_r : forall n m p : Z, n - p <= m <-> n <= m + p.
+Theorem Zle_sub_le_add_r : forall n m p : Z, n - p <= m <-> n <= m + p.
 Proof.
 intros n m p. stepl (n - p + p <= m + p) by symmetry; apply Zadd_le_mono_r.
-now rewrite Zminus_simpl_r.
+now rewrite Zsub_simpl_r.
 Qed.
 
-Theorem Zlt_minus_lt_add_l : forall n m p : Z, n - m < p <-> n < m + p.
+Theorem Zlt_sub_lt_add_l : forall n m p : Z, n - m < p <-> n < m + p.
 Proof.
-intros n m p. rewrite Zadd_comm; apply Zlt_minus_lt_add_r.
+intros n m p. rewrite Zadd_comm; apply Zlt_sub_lt_add_r.
 Qed.
 
-Theorem Zle_minus_le_add_l : forall n m p : Z, n - m <= p <-> n <= m + p.
+Theorem Zle_sub_le_add_l : forall n m p : Z, n - m <= p <-> n <= m + p.
 Proof.
-intros n m p. rewrite Zadd_comm; apply Zle_minus_le_add_r.
+intros n m p. rewrite Zadd_comm; apply Zle_sub_le_add_r.
 Qed.
 
-Theorem Zlt_minus_lt_add : forall n m p q : Z, n - m < p - q <-> n + q < m + p.
+Theorem Zlt_sub_lt_add : forall n m p q : Z, n - m < p - q <-> n + q < m + p.
 Proof.
-intros n m p q. rewrite Zlt_minus_lt_add_l. rewrite Zadd_minus_assoc.
-now rewrite <- Zlt_add_lt_minus_r.
+intros n m p q. rewrite Zlt_sub_lt_add_l. rewrite Zadd_sub_assoc.
+now rewrite <- Zlt_add_lt_sub_r.
 Qed.
 
-Theorem Zle_minus_le_add : forall n m p q : Z, n - m <= p - q <-> n + q <= m + p.
+Theorem Zle_sub_le_add : forall n m p q : Z, n - m <= p - q <-> n + q <= m + p.
 Proof.
-intros n m p q. rewrite Zle_minus_le_add_l. rewrite Zadd_minus_assoc.
-now rewrite <- Zle_add_le_minus_r.
+intros n m p q. rewrite Zle_sub_le_add_l. rewrite Zadd_sub_assoc.
+now rewrite <- Zle_add_le_sub_r.
 Qed.
 
-Theorem Zlt_minus_pos : forall n m : Z, 0 < m <-> n - m < n.
+Theorem Zlt_sub_pos : forall n m : Z, 0 < m <-> n - m < n.
 Proof.
-intros n m. stepr (n - m < n - 0) by now rewrite Zminus_0_r. apply Zminus_lt_mono_l.
+intros n m. stepr (n - m < n - 0) by now rewrite Zsub_0_r. apply Zsub_lt_mono_l.
 Qed.
 
-Theorem Zle_minus_nonneg : forall n m : Z, 0 <= m <-> n - m <= n.
+Theorem Zle_sub_nonneg : forall n m : Z, 0 <= m <-> n - m <= n.
 Proof.
-intros n m. stepr (n - m <= n - 0) by now rewrite Zminus_0_r. apply Zminus_le_mono_l.
+intros n m. stepr (n - m <= n - 0) by now rewrite Zsub_0_r. apply Zsub_le_mono_l.
 Qed.
 
-Theorem Zminus_lt_cases : forall n m p q : Z, n - m < p - q -> n < m \/ q < p.
+Theorem Zsub_lt_cases : forall n m p q : Z, n - m < p - q -> n < m \/ q < p.
 Proof.
-intros n m p q H. rewrite Zlt_minus_lt_add in H. now apply Zadd_lt_cases.
+intros n m p q H. rewrite Zlt_sub_lt_add in H. now apply Zadd_lt_cases.
 Qed.
 
-Theorem Zminus_le_cases : forall n m p q : Z, n - m <= p - q -> n <= m \/ q <= p.
+Theorem Zsub_le_cases : forall n m p q : Z, n - m <= p - q -> n <= m \/ q <= p.
 Proof.
-intros n m p q H. rewrite Zle_minus_le_add in H. now apply Zadd_le_cases.
+intros n m p q H. rewrite Zle_sub_le_add in H. now apply Zadd_le_cases.
 Qed.
 
-Theorem Zminus_neg_cases : forall n m : Z, n - m < 0 -> n < 0 \/ 0 < m.
+Theorem Zsub_neg_cases : forall n m : Z, n - m < 0 -> n < 0 \/ 0 < m.
 Proof.
 intros n m H; rewrite <- Zadd_opp_r in H.
 setoid_replace (0 < m) with (- m < 0) using relation iff by (symmetry; apply Zopp_neg_pos).
 now apply Zadd_neg_cases.
 Qed.
 
-Theorem Zminus_pos_cases : forall n m : Z, 0 < n - m -> 0 < n \/ m < 0.
+Theorem Zsub_pos_cases : forall n m : Z, 0 < n - m -> 0 < n \/ m < 0.
 Proof.
 intros n m H; rewrite <- Zadd_opp_r in H.
 setoid_replace (m < 0) with (0 < - m) using relation iff by (symmetry; apply Zopp_pos_neg).
 now apply Zadd_pos_cases.
 Qed.
 
-Theorem Zminus_nonpos_cases : forall n m : Z, n - m <= 0 -> n <= 0 \/ 0 <= m.
+Theorem Zsub_nonpos_cases : forall n m : Z, n - m <= 0 -> n <= 0 \/ 0 <= m.
 Proof.
 intros n m H; rewrite <- Zadd_opp_r in H.
 setoid_replace (0 <= m) with (- m <= 0) using relation iff by (symmetry; apply Zopp_nonpos_nonneg).
 now apply Zadd_nonpos_cases.
 Qed.
 
-Theorem Zminus_nonneg_cases : forall n m : Z, 0 <= n - m -> 0 <= n \/ m <= 0.
+Theorem Zsub_nonneg_cases : forall n m : Z, 0 <= n - m -> 0 <= n \/ m <= 0.
 Proof.
 intros n m H; rewrite <- Zadd_opp_r in H.
 setoid_replace (m <= 0) with (0 <= - m) using relation iff by (symmetry; apply Zopp_nonneg_nonpos).
@@ -368,6 +368,6 @@ End PosNeg.
 
 Ltac Z0_pos_neg n := induction_maker n ltac:(apply Z0_pos_neg).
 
-End ZPlusOrderPropFunct.
+End ZAddOrderPropFunct.
 
 
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 19fb40dfe..dfffe9a7f 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -26,7 +26,7 @@ Notation S := NZsucc.
 Notation P := NZpred.
 Notation Zadd := NZadd.
 Notation Zmul := NZmul.
-Notation Zminus := NZminus.
+Notation Zsub := NZsub.
 Notation Zlt := NZlt.
 Notation Zle := NZle.
 Notation Zmin := NZmin.
@@ -36,7 +36,7 @@ Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope.
 Notation "0" := NZ0 : IntScope.
 Notation "1" := (NZsucc NZ0) : IntScope.
 Notation "x + y" := (NZadd x y) : IntScope.
-Notation "x - y" := (NZminus x y) : IntScope.
+Notation "x - y" := (NZsub x y) : IntScope.
 Notation "x * y" := (NZmul x y) : IntScope.
 Notation "x < y" := (NZlt x y) : IntScope.
 Notation "x <= y" := (NZle x y) : IntScope.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 0b8538873..d175c358c 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -12,7 +12,7 @@
 
 Require Export Decidable.
 Require Export ZAxioms.
-Require Import NZTimesOrder.
+Require Import NZMulOrder.
 
 Module ZBasePropFunct (Import ZAxiomsMod : ZAxiomsSig).
 
@@ -22,7 +22,7 @@ notations in Zadd and later *)
 
 Open Local Scope IntScope.
 
-Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod.
+Module Export NZMulOrderMod := NZMulOrderPropFunct NZOrdAxiomsMod.
 
 Theorem Zsucc_wd : forall n1 n2 : Z, n1 == n2 -> S n1 == S n2.
 Proof NZsucc_wd.
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index 8ceecdbf2..1b8bdda40 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -10,10 +10,10 @@
 
 (*i $Id$ i*)
 
-Require Export ZTimes.
+Require Export ZMul.
 
 Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
-Module Export ZTimesPropMod := ZTimesPropFunct ZAxiomsMod.
+Module Export ZMulPropMod := ZMulPropFunct ZAxiomsMod.
 Open Local Scope IntScope.
 
 (* Axioms *)
diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZMul.v
index ccf324a06..785c0f41b 100644
--- a/theories/Numbers/Integer/Abstract/ZTimes.v
+++ b/theories/Numbers/Integer/Abstract/ZMul.v
@@ -10,10 +10,10 @@
 
 (*i $Id$ i*)
 
-Require Export ZPlus.
+Require Export ZAdd.
 
-Module ZTimesPropFunct (Import ZAxiomsMod : ZAxiomsSig).
-Module Export ZPlusPropMod := ZPlusPropFunct ZAxiomsMod.
+Module ZMulPropFunct (Import ZAxiomsMod : ZAxiomsSig).
+Module Export ZAddPropMod := ZAddPropFunct ZAxiomsMod.
 Open Local Scope IntScope.
 
 Theorem Zmul_wd :
@@ -74,7 +74,7 @@ Theorem Zmul_pred_r : forall n m : Z, n * (P m) == n * m - n.
 Proof.
 intros n m.
 rewrite <- (Zsucc_pred m) at 2.
-now rewrite Zmul_succ_r, <- Zadd_minus_assoc, Zminus_diag, Zadd_0_r.
+now rewrite Zmul_succ_r, <- Zadd_sub_assoc, Zsub_diag, Zadd_0_r.
 Qed.
 
 Theorem Zmul_pred_l : forall n m : Z, (P n) * m == n * m - m.
@@ -98,18 +98,18 @@ Proof.
 intros n m; now rewrite Zmul_opp_l, Zmul_opp_r, Zopp_involutive.
 Qed.
 
-Theorem Zmul_minus_distr_l : forall n m p : Z, n * (m - p) == n * m - n * p.
+Theorem Zmul_sub_distr_l : forall n m p : Z, n * (m - p) == n * m - n * p.
 Proof.
 intros n m p. do 2 rewrite <- Zadd_opp_r. rewrite Zmul_add_distr_l.
 now rewrite Zmul_opp_r.
 Qed.
 
-Theorem Zmul_minus_distr_r : forall n m p : Z, (n - m) * p == n * p - m * p.
+Theorem Zmul_sub_distr_r : forall n m p : Z, (n - m) * p == n * p - m * p.
 Proof.
 intros n m p; rewrite (Zmul_comm (n - m) p), (Zmul_comm n p), (Zmul_comm m p);
-now apply Zmul_minus_distr_l.
+now apply Zmul_sub_distr_l.
 Qed.
 
-End ZTimesPropFunct.
+End ZMulPropFunct.
 
 
diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index d3f5a0396..46a8a38af 100644
--- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -10,10 +10,10 @@
 
 (*i $Id$ i*)
 
-Require Export ZPlusOrder.
+Require Export ZAddOrder.
 
-Module ZTimesOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
-Module Export ZPlusOrderPropMod := ZPlusOrderPropFunct ZAxiomsMod.
+Module ZMulOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
+Module Export ZAddOrderPropMod := ZAddOrderPropFunct ZAxiomsMod.
 Open Local Scope IntScope.
 
 Theorem Zmul_lt_pred :
@@ -339,5 +339,5 @@ apply Zmul_lt_mono_nonneg.
 now apply Zlt_le_incl. assumption. apply Zle_0_1. assumption.
 Qed.
 
-End ZTimesOrderPropFunct.
+End ZMulOrderPropFunct.
 
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index f54737036..947dc818e 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -11,7 +11,7 @@
 (*i $Id$ i*)
 
 Require Export BigN.
-Require Import ZTimesOrder.
+Require Import ZMulOrder.
 Require Import ZSig.
 Require Import ZSigZAxioms.
 Require Import ZMake.
@@ -21,7 +21,7 @@ Module BigZ <: ZType := ZMake.Make BigN.
 (** Module [BigZ] implements [ZAxiomsSig] *)
 
 Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ.
-Module Export BigZTimesOrderPropMod := ZTimesOrderPropFunct BigZAxiomsMod.
+Module Export BigZMulOrderPropMod := ZMulOrderPropFunct BigZAxiomsMod.
 
 (** Notations about [BigZ] *)
 
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index acc77b3e7..0ff896367 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -10,7 +10,7 @@
 
 (*i $Id$ i*)
 
-Require Import ZTimesOrder.
+Require Import ZMulOrder.
 Require Import ZArith.
 
 Open Local Scope Z_scope.
@@ -25,7 +25,7 @@ Definition NZ0 := 0.
 Definition NZsucc := Zsucc'.
 Definition NZpred := Zpred'.
 Definition NZadd := Zplus.
-Definition NZminus := Zminus.
+Definition NZsub := Zminus.
 Definition NZmul := Zmult.
 
 Theorem NZeq_equiv : equiv Z NZeq.
@@ -54,7 +54,7 @@ Proof.
 congruence.
 Qed.
 
-Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd.
+Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.
 Proof.
 congruence.
 Qed.
@@ -89,12 +89,12 @@ Proof.
 intros; do 2 rewrite <- Zsucc_succ'; apply Zplus_succ_l.
 Qed.
 
-Theorem NZminus_0_r : forall n : Z, n - 0 = n.
+Theorem NZsub_0_r : forall n : Z, n - 0 = n.
 Proof.
 exact Zminus_0_r.
 Qed.
 
-Theorem NZminus_succ_r : forall n m : Z, n - (NZsucc m) = NZpred (n - m).
+Theorem NZsub_succ_r : forall n m : Z, n - (NZsucc m) = NZpred (n - m).
 Proof.
 intros; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred';
 apply Zminus_succ_r.
@@ -213,11 +213,11 @@ Qed.
 
 End ZBinAxiomsMod.
 
-Module Export ZBinTimesOrderPropMod := ZTimesOrderPropFunct ZBinAxiomsMod.
+Module Export ZBinMulOrderPropMod := ZMulOrderPropFunct ZBinAxiomsMod.
 
 (** Z forms a ring *)
 
-(*Lemma Zring : ring_theory 0 1 NZadd NZmul NZminus Zopp NZeq.
+(*Lemma Zring : ring_theory 0 1 NZadd NZmul NZsub Zopp NZeq.
 Proof.
 constructor.
 exact Zadd_0_l.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 97a72e087..aa027103f 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -10,15 +10,15 @@
 
 (*i $Id$ i*)
 
-Require Import NMinus. (* The most complete file for natural numbers *)
-Require Export ZTimesOrder. (* The most complete file for integers *)
+Require Import NSub. (* The most complete file for natural numbers *)
+Require Export ZMulOrder. (* The most complete file for integers *)
 Require Export Ring.
 
 Module ZPairsAxiomsMod (Import NAxiomsMod : NAxiomsSig) <: ZAxiomsSig.
-Module Import NPropMod := NMinusPropFunct NAxiomsMod. (* Get all properties of natural numbers *)
+Module Import NPropMod := NSubPropFunct NAxiomsMod. (* Get all properties of natural numbers *)
 
 (* We do not declare ring in Natural/Abstract for two reasons. First, some
-of the properties proved in NPlus and NTimes are used in the new BinNat,
+of the properties proved in NAdd and NMul are used in the new BinNat,
 and it is in turn used in Ring. Using ring in Natural/Abstract would be
 circular. It is possible, however, not to make BinNat dependent on
 Numbers/Natural and prove the properties necessary for ring from scratch
@@ -62,7 +62,7 @@ canonical values. In that case, we could get rid of setoids and arrive at
 integers as signed natural numbers. *)
 
 Definition Zadd (n m : Z) : Z := ((fst n) + (fst m), (snd n) + (snd m)).
-Definition Zminus (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst m)).
+Definition Zsub (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst m)).
 
 (* Unfortunately, the elements of the pair keep increasing, even during
 subtraction *)
@@ -81,7 +81,7 @@ Notation "x ~= y" := (~ Zeq x y) (at level 70) : IntScope.
 Notation "0" := Z0 : IntScope.
 Notation "1" := (Zsucc Z0) : IntScope.
 Notation "x + y" := (Zadd x y) : IntScope.
-Notation "x - y" := (Zminus x y) : IntScope.
+Notation "x - y" := (Zsub x y) : IntScope.
 Notation "x * y" := (Zmul x y) : IntScope.
 Notation "x < y" := (Zlt x y) : IntScope.
 Notation "x <= y" := (Zle x y) : IntScope.
@@ -102,7 +102,7 @@ Definition NZ0 := Z0.
 Definition NZsucc := Zsucc.
 Definition NZpred := Zpred.
 Definition NZadd := Zadd.
-Definition NZminus := Zminus.
+Definition NZsub := Zsub.
 Definition NZmul := Zmul.
 
 Theorem ZE_refl : reflexive Z Zeq.
@@ -162,9 +162,9 @@ 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 Zeq ==> Zeq ==> Zeq as NZminus_wd.
+Add Morphism NZsub with signature Zeq ==> Zeq ==> Zeq as NZsub_wd.
 Proof.
-unfold Zeq, NZminus; intros n1 m1 H1 n2 m2 H2; simpl.
+unfold Zeq, NZsub; 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 add_wd.
@@ -243,14 +243,14 @@ Proof.
 intros n m; unfold NZadd, Zeq; simpl. now do 2 rewrite add_succ_l.
 Qed.
 
-Theorem NZminus_0_r : forall n : Z, n - 0 == n.
+Theorem NZsub_0_r : forall n : Z, n - 0 == n.
 Proof.
-intro n; unfold NZminus, Zeq; simpl. now do 2 rewrite add_0_r.
+intro n; unfold NZsub, Zeq; simpl. now do 2 rewrite add_0_r.
 Qed.
 
-Theorem NZminus_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m).
+Theorem NZsub_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m).
 Proof.
-intros n m; unfold NZminus, Zeq; simpl. symmetry; now rewrite add_succ_r.
+intros n m; unfold NZsub, Zeq; simpl. symmetry; now rewrite add_succ_r.
 Qed.
 
 Theorem NZmul_0_l : forall n : Z, 0 * n == 0.
@@ -413,7 +413,7 @@ and get their properties *)
 Require Import NPeano.
 
 Module Export ZPairsPeanoAxiomsMod := ZPairsAxiomsMod NPeanoAxiomsMod.
-Module Export ZPairsTimesOrderPropMod := ZTimesOrderPropFunct ZPairsPeanoAxiomsMod.
+Module Export ZPairsMulOrderPropMod := ZMulOrderPropFunct ZPairsPeanoAxiomsMod.
 
 Open Local Scope IntScope.
 
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index bb56e6997..e1f04e45a 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -42,7 +42,7 @@ Definition NZ0 := Z.zero.
 Definition NZsucc := Z.succ.
 Definition NZpred := Z.pred.
 Definition NZadd := Z.add.
-Definition NZminus := Z.sub.
+Definition NZsub := Z.sub.
 Definition NZmul := Z.mul.
 
 Theorem NZeq_equiv : equiv Z.t Z.eq.
@@ -71,7 +71,7 @@ Proof.
 intros; zsimpl; f_equal; assumption.
 Qed.
 
-Add Morphism NZminus with signature Z.eq ==> Z.eq ==> Z.eq as NZminus_wd.
+Add Morphism NZsub with signature Z.eq ==> Z.eq ==> Z.eq as NZsub_wd.
 Proof.
 intros; zsimpl; f_equal; assumption.
 Qed.
@@ -154,12 +154,12 @@ Proof.
 intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem NZminus_0_r : forall n, n - 0 == n.
+Theorem NZsub_0_r : forall n, n - 0 == n.
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem NZminus_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m).
+Theorem NZsub_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m).
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.