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

for increased consistency with bignums parts 

(commit part I: content of files)



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

10 files changed, 479 insertions, 479 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 678781b23..19fb40dfe 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -24,8 +24,8 @@ Notation Z0 := NZ0.
 Notation Z1 := (NZsucc NZ0).
 Notation S := NZsucc.
 Notation P := NZpred.
-Notation Zplus := NZplus.
-Notation Ztimes := NZtimes.
+Notation Zadd := NZadd.
+Notation Zmul := NZmul.
 Notation Zminus := NZminus.
 Notation Zlt := NZlt.
 Notation Zle := NZle.
@@ -35,9 +35,9 @@ Notation "x == y"  := (NZeq x y) (at level 70) : IntScope.
 Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope.
 Notation "0" := NZ0 : IntScope.
 Notation "1" := (NZsucc NZ0) : IntScope.
-Notation "x + y" := (NZplus x y) : IntScope.
+Notation "x + y" := (NZadd x y) : IntScope.
 Notation "x - y" := (NZminus x y) : IntScope.
-Notation "x * y" := (NZtimes x y) : IntScope.
+Notation "x * y" := (NZmul x y) : IntScope.
 Notation "x < y" := (NZlt x y) : IntScope.
 Notation "x <= y" := (NZle x y) : IntScope.
 Notation "x > y" := (NZlt y x) (only parsing) : IntScope.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index c57f9ede0..0b8538873 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -18,7 +18,7 @@ Module ZBasePropFunct (Import ZAxiomsMod : ZAxiomsSig).
 
 (* Note: writing "Export" instead of "Import" on the previous line leads to
 some warnings about hiding repeated declarations and results in the loss of
-notations in Zplus and later *)
+notations in Zadd and later *)
 
 Open Local Scope IntScope.
 
diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v
index 2520d62e1..d72d00379 100644
--- a/theories/Numbers/Integer/Abstract/ZPlus.v
+++ b/theories/Numbers/Integer/Abstract/ZPlus.v
@@ -16,15 +16,15 @@ Module ZPlusPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZBasePropMod := ZBasePropFunct ZAxiomsMod.
 Open Local Scope IntScope.
 
-Theorem Zplus_wd :
+Theorem Zadd_wd :
   forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 + m1 == n2 + m2.
-Proof NZplus_wd.
+Proof NZadd_wd.
 
-Theorem Zplus_0_l : forall n : Z, 0 + n == n.
-Proof NZplus_0_l.
+Theorem Zadd_0_l : forall n : Z, 0 + n == n.
+Proof NZadd_0_l.
 
-Theorem Zplus_succ_l : forall n m : Z, (S n) + m == S (n + m).
-Proof NZplus_succ_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.
@@ -40,66 +40,66 @@ Proof Zopp_succ.
 
 (* Theorems that are valid for both natural numbers and integers *)
 
-Theorem Zplus_0_r : forall n : Z, n + 0 == n.
-Proof NZplus_0_r.
+Theorem Zadd_0_r : forall n : Z, n + 0 == n.
+Proof NZadd_0_r.
 
-Theorem Zplus_succ_r : forall n m : Z, n + S m == S (n + m).
-Proof NZplus_succ_r.
+Theorem Zadd_succ_r : forall n m : Z, n + S m == S (n + m).
+Proof NZadd_succ_r.
 
-Theorem Zplus_comm : forall n m : Z, n + m == m + n.
-Proof NZplus_comm.
+Theorem Zadd_comm : forall n m : Z, n + m == m + n.
+Proof NZadd_comm.
 
-Theorem Zplus_assoc : forall n m p : Z, n + (m + p) == (n + m) + p.
-Proof NZplus_assoc.
+Theorem Zadd_assoc : forall n m p : Z, n + (m + p) == (n + m) + p.
+Proof NZadd_assoc.
 
-Theorem Zplus_shuffle1 : forall n m p q : Z, (n + m) + (p + q) == (n + p) + (m + q).
-Proof NZplus_shuffle1.
+Theorem Zadd_shuffle1 : forall n m p q : Z, (n + m) + (p + q) == (n + p) + (m + q).
+Proof NZadd_shuffle1.
 
-Theorem Zplus_shuffle2 : forall n m p q : Z, (n + m) + (p + q) == (n + q) + (m + p).
-Proof NZplus_shuffle2.
+Theorem Zadd_shuffle2 : forall n m p q : Z, (n + m) + (p + q) == (n + q) + (m + p).
+Proof NZadd_shuffle2.
 
-Theorem Zplus_1_l : forall n : Z, 1 + n == S n.
-Proof NZplus_1_l.
+Theorem Zadd_1_l : forall n : Z, 1 + n == S n.
+Proof NZadd_1_l.
 
-Theorem Zplus_1_r : forall n : Z, n + 1 == S n.
-Proof NZplus_1_r.
+Theorem Zadd_1_r : forall n : Z, n + 1 == S n.
+Proof NZadd_1_r.
 
-Theorem Zplus_cancel_l : forall n m p : Z, p + n == p + m <-> n == m.
-Proof NZplus_cancel_l.
+Theorem Zadd_cancel_l : forall n m p : Z, p + n == p + m <-> n == m.
+Proof NZadd_cancel_l.
 
-Theorem Zplus_cancel_r : forall n m p : Z, n + p == m + p <-> n == m.
-Proof NZplus_cancel_r.
+Theorem Zadd_cancel_r : forall n m p : Z, n + p == m + p <-> n == m.
+Proof NZadd_cancel_r.
 
 (* Theorems that are either not valid on N or have different proofs on N and Z *)
 
-Theorem Zplus_pred_l : forall n m : Z, P n + m == P (n + m).
+Theorem Zadd_pred_l : forall n m : Z, P n + m == P (n + m).
 Proof.
 intros n m.
 rewrite <- (Zsucc_pred n) at 2.
-rewrite Zplus_succ_l. now rewrite Zpred_succ.
+rewrite Zadd_succ_l. now rewrite Zpred_succ.
 Qed.
 
-Theorem Zplus_pred_r : forall n m : Z, n + P m == P (n + m).
+Theorem Zadd_pred_r : forall n m : Z, n + P m == P (n + m).
 Proof.
-intros n m; rewrite (Zplus_comm n (P m)), (Zplus_comm n m);
-apply Zplus_pred_l.
+intros n m; rewrite (Zadd_comm n (P m)), (Zadd_comm n m);
+apply Zadd_pred_l.
 Qed.
 
-Theorem Zplus_opp_r : forall n m : Z, n + (- m) == n - m.
+Theorem Zadd_opp_r : forall n m : Z, n + (- m) == n - m.
 Proof.
 NZinduct m.
-rewrite Zopp_0; rewrite Zminus_0_r; now rewrite Zplus_0_r.
-intro m. rewrite Zopp_succ, Zminus_succ_r, Zplus_pred_r; now rewrite Zpred_inj_wd.
+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.
 Qed.
 
 Theorem Zminus_0_l : forall n : Z, 0 - n == - n.
 Proof.
-intro n; rewrite <- Zplus_opp_r; now rewrite Zplus_0_l.
+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).
 Proof.
-intros n m; do 2 rewrite <- Zplus_opp_r; now rewrite Zplus_succ_l.
+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).
@@ -127,24 +127,24 @@ now rewrite Zminus_0_r.
 intro n. rewrite Zminus_succ_r, Zminus_succ_l; now rewrite Zpred_succ.
 Qed.
 
-Theorem Zplus_opp_diag_l : forall n : Z, - n + n == 0.
+Theorem Zadd_opp_diag_l : forall n : Z, - n + n == 0.
 Proof.
-intro n; now rewrite Zplus_comm, Zplus_opp_r, Zminus_diag.
+intro n; now rewrite Zadd_comm, Zadd_opp_r, Zminus_diag.
 Qed.
 
-Theorem Zplus_opp_diag_r : forall n : Z, n + (- n) == 0.
+Theorem Zadd_opp_diag_r : forall n : Z, n + (- n) == 0.
 Proof.
-intro n; rewrite Zplus_comm; apply Zplus_opp_diag_l.
+intro n; rewrite Zadd_comm; apply Zadd_opp_diag_l.
 Qed.
 
-Theorem Zplus_opp_l : forall n m : Z, - m + n == n - m.
+Theorem Zadd_opp_l : forall n m : Z, - m + n == n - m.
 Proof.
-intros n m; rewrite <- Zplus_opp_r; now rewrite Zplus_comm.
+intros n m; rewrite <- Zadd_opp_r; now rewrite Zadd_comm.
 Qed.
 
-Theorem Zplus_minus_assoc : forall n m p : Z, n + (m - p) == (n + m) - p.
+Theorem Zadd_minus_assoc : forall n m p : Z, n + (m - p) == (n + m) - p.
 Proof.
-intros n m p; do 2 rewrite <- Zplus_opp_r; now rewrite Zplus_assoc.
+intros n m p; do 2 rewrite <- Zadd_opp_r; now rewrite Zadd_assoc.
 Qed.
 
 Theorem Zopp_involutive : forall n : Z, - (- n) == n.
@@ -154,17 +154,17 @@ now do 2 rewrite Zopp_0.
 intro n. rewrite Zopp_succ, Zopp_pred; now rewrite Zsucc_inj_wd.
 Qed.
 
-Theorem Zopp_plus_distr : forall n m : Z, - (n + m) == - n + (- m).
+Theorem Zopp_add_distr : forall n m : Z, - (n + m) == - n + (- m).
 Proof.
 intros n m; NZinduct n.
-rewrite Zopp_0; now do 2 rewrite Zplus_0_l.
-intro n. rewrite Zplus_succ_l; do 2 rewrite Zopp_succ; rewrite Zplus_pred_l.
+rewrite Zopp_0; now do 2 rewrite Zadd_0_l.
+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.
 Proof.
-intros n m; rewrite <- Zplus_opp_r, Zopp_plus_distr.
+intros n m; rewrite <- Zadd_opp_r, Zopp_add_distr.
 now rewrite Zopp_involutive.
 Qed.
 
@@ -188,63 +188,63 @@ Proof.
 symmetry; apply Zeq_opp_l.
 Qed.
 
-Theorem Zminus_plus_distr : forall n m p : Z, n - (m + p) == (n - m) - p.
+Theorem Zminus_add_distr : forall n m p : Z, n - (m + p) == (n - m) - p.
 Proof.
-intros n m p; rewrite <- Zplus_opp_r, Zopp_plus_distr, Zplus_assoc.
-now do 2 rewrite Zplus_opp_r.
+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.
 Proof.
-intros n m p; rewrite <- Zplus_opp_r, Zopp_minus_distr, Zplus_assoc.
-now rewrite Zplus_opp_r.
+intros n m p; rewrite <- Zadd_opp_r, Zopp_minus_distr, Zadd_assoc.
+now rewrite Zadd_opp_r.
 Qed.
 
 Theorem minus_opp_l : forall n m : Z, - n - m == - m - n.
 Proof.
-intros n m. do 2 rewrite <- Zplus_opp_r. now rewrite Zplus_comm.
+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.
 Proof.
-intros n m; rewrite <- Zplus_opp_r; now rewrite Zopp_involutive.
+intros n m; rewrite <- Zadd_opp_r; now rewrite Zopp_involutive.
 Qed.
 
-Theorem Zplus_minus_swap : forall n m p : Z, n + m - p == n - p + m.
+Theorem Zadd_minus_swap : forall n m p : Z, n + m - p == n - p + m.
 Proof.
-intros n m p. rewrite <- Zplus_minus_assoc, <- (Zplus_opp_r n p), <- Zplus_assoc.
-now rewrite Zplus_opp_l.
+intros n m p. rewrite <- Zadd_minus_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.
 Proof.
-intros n m p. rewrite <- (Zplus_cancel_l (n - m) (n - p) (- n)).
-do 2 rewrite Zplus_minus_assoc. rewrite Zplus_opp_diag_l; do 2 rewrite Zminus_0_l.
+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.
 apply Zopp_inj_wd.
 Qed.
 
 Theorem Zminus_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 Zplus_cancel_r.
+stepl (n - p + p == m - p + p) by apply Zadd_cancel_r.
 now do 2 rewrite <- Zminus_minus_distr, Zminus_diag, Zminus_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 (plus or minus) and the indication whether the left or right term
+equation (add or minus) and the indication whether the left or right term
 is moved. *)
 
-Theorem Zplus_move_l : forall n m p : Z, n + m == p <-> m == p - n.
+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 Zplus_comm, <- Zplus_minus_assoc, Zminus_diag, Zplus_0_r.
+now rewrite Zadd_comm, <- Zadd_minus_assoc, Zminus_diag, Zadd_0_r.
 Qed.
 
-Theorem Zplus_move_r : forall n m p : Z, n + m == p <-> n == p - m.
+Theorem Zadd_move_r : forall n m p : Z, n + m == p <-> n == p - m.
 Proof.
-intros n m p; rewrite Zplus_comm; now apply Zplus_move_l.
+intros n m p; rewrite Zadd_comm; now apply Zadd_move_l.
 Qed.
 
 (* The two theorems above do not allow rewriting subformulas of the form
@@ -253,22 +253,22 @@ the equation. Hence the following two theorems. *)
 
 Theorem Zminus_move_l : forall n m p : Z, n - m == p <-> - m == p - n.
 Proof.
-intros n m p; rewrite <- (Zplus_opp_r n m); apply Zplus_move_l.
+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.
 Proof.
-intros n m p; rewrite <- (Zplus_opp_r n m). now rewrite Zplus_move_r, Zminus_opp_r.
+intros n m p; rewrite <- (Zadd_opp_r n m). now rewrite Zadd_move_r, Zminus_opp_r.
 Qed.
 
-Theorem Zplus_move_0_l : forall n m : Z, n + m == 0 <-> m == - n.
+Theorem Zadd_move_0_l : forall n m : Z, n + m == 0 <-> m == - n.
 Proof.
-intros n m; now rewrite Zplus_move_l, Zminus_0_l.
+intros n m; now rewrite Zadd_move_l, Zminus_0_l.
 Qed.
 
-Theorem Zplus_move_0_r : forall n m : Z, n + m == 0 <-> n == - m.
+Theorem Zadd_move_0_r : forall n m : Z, n + m == 0 <-> n == - m.
 Proof.
-intros n m; now rewrite Zplus_move_r, Zminus_0_l.
+intros n m; now rewrite Zadd_move_r, Zminus_0_l.
 Qed.
 
 Theorem Zminus_move_0_l : forall n m : Z, n - m == 0 <-> - m == - n.
@@ -278,25 +278,25 @@ Qed.
 
 Theorem Zminus_move_0_r : forall n m : Z, n - m == 0 <-> n == m.
 Proof.
-intros n m. now rewrite Zminus_move_r, Zplus_0_l.
+intros n m. now rewrite Zminus_move_r, Zadd_0_l.
 Qed.
 
 (* The following section is devoted to cancellation of like terms. The name
 includes the first operator and the position of the term being canceled. *)
 
-Theorem Zplus_simpl_l : forall n m : Z, n + m - n == m.
+Theorem Zadd_simpl_l : forall n m : Z, n + m - n == m.
 Proof.
-intros; now rewrite Zplus_minus_swap, Zminus_diag, Zplus_0_l.
+intros; now rewrite Zadd_minus_swap, Zminus_diag, Zadd_0_l.
 Qed.
 
-Theorem Zplus_simpl_r : forall n m : Z, n + m - m == n.
+Theorem Zadd_simpl_r : forall n m : Z, n + m - m == n.
 Proof.
-intros; now rewrite <- Zplus_minus_assoc, Zminus_diag, Zplus_0_r.
+intros; now rewrite <- Zadd_minus_assoc, Zminus_diag, Zadd_0_r.
 Qed.
 
 Theorem Zminus_simpl_l : forall n m : Z, - n - m + n == - m.
 Proof.
-intros; now rewrite <- Zplus_minus_swap, Zplus_opp_diag_l, Zminus_0_l.
+intros; now rewrite <- Zadd_minus_swap, Zadd_opp_diag_l, Zminus_0_l.
 Qed.
 
 Theorem Zminus_simpl_r : forall n m : Z, n - m + m == n.
@@ -307,36 +307,36 @@ Qed.
 (* Now we have two sums or differences; the name includes the two operators
 and the position of the terms being canceled *)
 
-Theorem Zplus_plus_simpl_l_l : forall n m p : Z, (n + m) - (n + p) == m - p.
+Theorem Zadd_add_simpl_l_l : forall n m p : Z, (n + m) - (n + p) == m - p.
 Proof.
-intros n m p. now rewrite (Zplus_comm n m), <- Zplus_minus_assoc,
-Zminus_plus_distr, Zminus_diag, Zminus_0_l, Zplus_opp_r.
+intros n m p. now rewrite (Zadd_comm n m), <- Zadd_minus_assoc,
+Zminus_add_distr, Zminus_diag, Zminus_0_l, Zadd_opp_r.
 Qed.
 
-Theorem Zplus_plus_simpl_l_r : forall n m p : Z, (n + m) - (p + n) == m - p.
+Theorem Zadd_add_simpl_l_r : forall n m p : Z, (n + m) - (p + n) == m - p.
 Proof.
-intros n m p. rewrite (Zplus_comm p n); apply Zplus_plus_simpl_l_l.
+intros n m p. rewrite (Zadd_comm p n); apply Zadd_add_simpl_l_l.
 Qed.
 
-Theorem Zplus_plus_simpl_r_l : forall n m p : Z, (n + m) - (m + p) == n - p.
+Theorem Zadd_add_simpl_r_l : forall n m p : Z, (n + m) - (m + p) == n - p.
 Proof.
-intros n m p. rewrite (Zplus_comm n m); apply Zplus_plus_simpl_l_l.
+intros n m p. rewrite (Zadd_comm n m); apply Zadd_add_simpl_l_l.
 Qed.
 
-Theorem Zplus_plus_simpl_r_r : forall n m p : Z, (n + m) - (p + m) == n - p.
+Theorem Zadd_add_simpl_r_r : forall n m p : Z, (n + m) - (p + m) == n - p.
 Proof.
-intros n m p. rewrite (Zplus_comm p m); apply Zplus_plus_simpl_r_l.
+intros n m p. rewrite (Zadd_comm p m); apply Zadd_add_simpl_r_l.
 Qed.
 
-Theorem Zminus_plus_simpl_r_l : forall n m p : Z, (n - m) + (m + p) == n + p.
+Theorem Zminus_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_plus_distr, Zminus_diag,
+intros n m p. now rewrite <- Zminus_minus_distr, Zminus_add_distr, Zminus_diag,
 Zminus_0_l, Zminus_opp_r.
 Qed.
 
-Theorem Zminus_plus_simpl_r_r : forall n m p : Z, (n - m) + (p + m) == n + p.
+Theorem Zminus_add_simpl_r_r : forall n m p : Z, (n - m) + (p + m) == n + p.
 Proof.
-intros n m p. rewrite (Zplus_comm p m); apply Zminus_plus_simpl_r_l.
+intros n m p. rewrite (Zadd_comm p m); apply Zminus_add_simpl_r_l.
 Qed.
 
 (* Of course, there are many other variants *)
diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
index 3e6421819..85f671498 100644
--- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
@@ -18,141 +18,141 @@ Open Local Scope IntScope.
 
 (* Theorems that are true on both natural numbers and integers *)
 
-Theorem Zplus_lt_mono_l : forall n m p : Z, n < m <-> p + n < p + m.
-Proof NZplus_lt_mono_l.
+Theorem Zadd_lt_mono_l : forall n m p : Z, n < m <-> p + n < p + m.
+Proof NZadd_lt_mono_l.
 
-Theorem Zplus_lt_mono_r : forall n m p : Z, n < m <-> n + p < m + p.
-Proof NZplus_lt_mono_r.
+Theorem Zadd_lt_mono_r : forall n m p : Z, n < m <-> n + p < m + p.
+Proof NZadd_lt_mono_r.
 
-Theorem Zplus_lt_mono : forall n m p q : Z, n < m -> p < q -> n + p < m + q.
-Proof NZplus_lt_mono.
+Theorem Zadd_lt_mono : forall n m p q : Z, n < m -> p < q -> n + p < m + q.
+Proof NZadd_lt_mono.
 
-Theorem Zplus_le_mono_l : forall n m p : Z, n <= m <-> p + n <= p + m.
-Proof NZplus_le_mono_l.
+Theorem Zadd_le_mono_l : forall n m p : Z, n <= m <-> p + n <= p + m.
+Proof NZadd_le_mono_l.
 
-Theorem Zplus_le_mono_r : forall n m p : Z, n <= m <-> n + p <= m + p.
-Proof NZplus_le_mono_r.
+Theorem Zadd_le_mono_r : forall n m p : Z, n <= m <-> n + p <= m + p.
+Proof NZadd_le_mono_r.
 
-Theorem Zplus_le_mono : forall n m p q : Z, n <= m -> p <= q -> n + p <= m + q.
-Proof NZplus_le_mono.
+Theorem Zadd_le_mono : forall n m p q : Z, n <= m -> p <= q -> n + p <= m + q.
+Proof NZadd_le_mono.
 
-Theorem Zplus_lt_le_mono : forall n m p q : Z, n < m -> p <= q -> n + p < m + q.
-Proof NZplus_lt_le_mono.
+Theorem Zadd_lt_le_mono : forall n m p q : Z, n < m -> p <= q -> n + p < m + q.
+Proof NZadd_lt_le_mono.
 
-Theorem Zplus_le_lt_mono : forall n m p q : Z, n <= m -> p < q -> n + p < m + q.
-Proof NZplus_le_lt_mono.
+Theorem Zadd_le_lt_mono : forall n m p q : Z, n <= m -> p < q -> n + p < m + q.
+Proof NZadd_le_lt_mono.
 
-Theorem Zplus_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n + m.
-Proof NZplus_pos_pos.
+Theorem Zadd_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n + m.
+Proof NZadd_pos_pos.
 
-Theorem Zplus_pos_nonneg : forall n m : Z, 0 < n -> 0 <= m -> 0 < n + m.
-Proof NZplus_pos_nonneg.
+Theorem Zadd_pos_nonneg : forall n m : Z, 0 < n -> 0 <= m -> 0 < n + m.
+Proof NZadd_pos_nonneg.
 
-Theorem Zplus_nonneg_pos : forall n m : Z, 0 <= n -> 0 < m -> 0 < n + m.
-Proof NZplus_nonneg_pos.
+Theorem Zadd_nonneg_pos : forall n m : Z, 0 <= n -> 0 < m -> 0 < n + m.
+Proof NZadd_nonneg_pos.
 
-Theorem Zplus_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n + m.
-Proof NZplus_nonneg_nonneg.
+Theorem Zadd_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n + m.
+Proof NZadd_nonneg_nonneg.
 
-Theorem Zlt_plus_pos_l : forall n m : Z, 0 < n -> m < n + m.
-Proof NZlt_plus_pos_l.
+Theorem Zlt_add_pos_l : forall n m : Z, 0 < n -> m < n + m.
+Proof NZlt_add_pos_l.
 
-Theorem Zlt_plus_pos_r : forall n m : Z, 0 < n -> m < m + n.
-Proof NZlt_plus_pos_r.
+Theorem Zlt_add_pos_r : forall n m : Z, 0 < n -> m < m + n.
+Proof NZlt_add_pos_r.
 
-Theorem Zle_lt_plus_lt : forall n m p q : Z, n <= m -> p + m < q + n -> p < q.
-Proof NZle_lt_plus_lt.
+Theorem Zle_lt_add_lt : forall n m p q : Z, n <= m -> p + m < q + n -> p < q.
+Proof NZle_lt_add_lt.
 
-Theorem Zlt_le_plus_lt : forall n m p q : Z, n < m -> p + m <= q + n -> p < q.
-Proof NZlt_le_plus_lt.
+Theorem Zlt_le_add_lt : forall n m p q : Z, n < m -> p + m <= q + n -> p < q.
+Proof NZlt_le_add_lt.
 
-Theorem Zle_le_plus_le : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q.
-Proof NZle_le_plus_le.
+Theorem Zle_le_add_le : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q.
+Proof NZle_le_add_le.
 
-Theorem Zplus_lt_cases : forall n m p q : Z, n + m < p + q -> n < p \/ m < q.
-Proof NZplus_lt_cases.
+Theorem Zadd_lt_cases : forall n m p q : Z, n + m < p + q -> n < p \/ m < q.
+Proof NZadd_lt_cases.
 
-Theorem Zplus_le_cases : forall n m p q : Z, n + m <= p + q -> n <= p \/ m <= q.
-Proof NZplus_le_cases.
+Theorem Zadd_le_cases : forall n m p q : Z, n + m <= p + q -> n <= p \/ m <= q.
+Proof NZadd_le_cases.
 
-Theorem Zplus_neg_cases : forall n m : Z, n + m < 0 -> n < 0 \/ m < 0.
-Proof NZplus_neg_cases.
+Theorem Zadd_neg_cases : forall n m : Z, n + m < 0 -> n < 0 \/ m < 0.
+Proof NZadd_neg_cases.
 
-Theorem Zplus_pos_cases : forall n m : Z, 0 < n + m -> 0 < n \/ 0 < m.
-Proof NZplus_pos_cases.
+Theorem Zadd_pos_cases : forall n m : Z, 0 < n + m -> 0 < n \/ 0 < m.
+Proof NZadd_pos_cases.
 
-Theorem Zplus_nonpos_cases : forall n m : Z, n + m <= 0 -> n <= 0 \/ m <= 0.
-Proof NZplus_nonpos_cases.
+Theorem Zadd_nonpos_cases : forall n m : Z, n + m <= 0 -> n <= 0 \/ m <= 0.
+Proof NZadd_nonpos_cases.
 
-Theorem Zplus_nonneg_cases : forall n m : Z, 0 <= n + m -> 0 <= n \/ 0 <= m.
-Proof NZplus_nonneg_cases.
+Theorem Zadd_nonneg_cases : forall n m : Z, 0 <= n + m -> 0 <= n \/ 0 <= m.
+Proof NZadd_nonneg_cases.
 
 (* Theorems that are either not valid on N or have different proofs on N and Z *)
 
-Theorem Zplus_neg_neg : forall n m : Z, n < 0 -> m < 0 -> n + m < 0.
+Theorem Zadd_neg_neg : forall n m : Z, n < 0 -> m < 0 -> n + m < 0.
 Proof.
-intros n m H1 H2. rewrite <- (Zplus_0_l 0). now apply Zplus_lt_mono.
+intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_lt_mono.
 Qed.
 
-Theorem Zplus_neg_nonpos : forall n m : Z, n < 0 -> m <= 0 -> n + m < 0.
+Theorem Zadd_neg_nonpos : forall n m : Z, n < 0 -> m <= 0 -> n + m < 0.
 Proof.
-intros n m H1 H2. rewrite <- (Zplus_0_l 0). now apply Zplus_lt_le_mono.
+intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_lt_le_mono.
 Qed.
 
-Theorem Zplus_nonpos_neg : forall n m : Z, n <= 0 -> m < 0 -> n + m < 0.
+Theorem Zadd_nonpos_neg : forall n m : Z, n <= 0 -> m < 0 -> n + m < 0.
 Proof.
-intros n m H1 H2. rewrite <- (Zplus_0_l 0). now apply Zplus_le_lt_mono.
+intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_le_lt_mono.
 Qed.
 
-Theorem Zplus_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> n + m <= 0.
+Theorem Zadd_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> n + m <= 0.
 Proof.
-intros n m H1 H2. rewrite <- (Zplus_0_l 0). now apply Zplus_le_mono.
+intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_le_mono.
 Qed.
 
 (** Minus and order *)
 
 Theorem Zlt_0_minus : forall n m : Z, 0 < m - n <-> n < m.
 Proof.
-intros n m. stepl (0 + n < m - n + n) by symmetry; apply Zplus_lt_mono_r.
-rewrite Zplus_0_l; now rewrite Zminus_simpl_r.
+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.
 Qed.
 
 Notation Zminus_pos := Zlt_0_minus (only parsing).
 
 Theorem Zle_0_minus : forall n m : Z, 0 <= m - n <-> n <= m.
 Proof.
-intros n m; stepl (0 + n <= m - n + n) by symmetry; apply Zplus_le_mono_r.
-rewrite Zplus_0_l; now rewrite Zminus_simpl_r.
+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.
 Qed.
 
 Notation Zminus_nonneg := Zle_0_minus (only parsing).
 
 Theorem Zlt_minus_0 : forall n m : Z, n - m < 0 <-> n < m.
 Proof.
-intros n m. stepl (n - m + m < 0 + m) by symmetry; apply Zplus_lt_mono_r.
-rewrite Zplus_0_l; now rewrite Zminus_simpl_r.
+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.
 Qed.
 
 Notation Zminus_neg := Zlt_minus_0 (only parsing).
 
 Theorem Zle_minus_0 : forall n m : Z, n - m <= 0 <-> n <= m.
 Proof.
-intros n m. stepl (n - m + m <= 0 + m) by symmetry; apply Zplus_le_mono_r.
-rewrite Zplus_0_l; now rewrite Zminus_simpl_r.
+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.
 Qed.
 
 Notation Zminus_nonpos := Zle_minus_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 Zplus_lt_mono_l.
-do 2 rewrite Zplus_opp_r. rewrite Zminus_diag. symmetry; apply Zlt_0_minus.
+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.
 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 Zplus_le_mono_l.
-do 2 rewrite Zplus_opp_r. rewrite Zminus_diag. symmetry; apply Zle_0_minus.
+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.
 Qed.
 
 Theorem Zopp_pos_neg : forall n : Z, 0 < - n <-> n < 0.
@@ -177,13 +177,13 @@ Qed.
 
 Theorem Zminus_lt_mono_l : forall n m p : Z, n < m <-> p - m < p - n.
 Proof.
-intros n m p. do 2 rewrite <- Zplus_opp_r. rewrite <- Zplus_lt_mono_l.
+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.
 Proof.
-intros n m p; do 2 rewrite <- Zplus_opp_r; apply Zplus_lt_mono_r.
+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.
@@ -195,13 +195,13 @@ Qed.
 
 Theorem Zminus_le_mono_l : forall n m p : Z, n <= m <-> p - m <= p - n.
 Proof.
-intros n m p; do 2 rewrite <- Zplus_opp_r; rewrite <- Zplus_le_mono_l;
+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.
 Proof.
-intros n m p; do 2 rewrite <- Zplus_opp_r; apply Zplus_le_mono_r.
+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.
@@ -227,76 +227,76 @@ Qed.
 
 Theorem Zle_lt_minus_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_plus_lt (- m) (- n));
-[now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_r].
+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.
 Proof.
-intros n m p q H1 H2. apply (Zlt_le_plus_lt (- m) (- n));
-[now apply -> Zopp_lt_mono | now do 2 rewrite Zplus_opp_r].
+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.
 Proof.
-intros n m p q H1 H2. apply (Zle_le_plus_le (- m) (- n));
-[now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_r].
+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_plus_lt_minus_r : forall n m p : Z, n + p < m <-> n < m - p.
+Theorem Zlt_add_lt_minus_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.
-now rewrite Zplus_simpl_r.
+now rewrite Zadd_simpl_r.
 Qed.
 
-Theorem Zle_plus_le_minus_r : forall n m p : Z, n + p <= m <-> n <= m - p.
+Theorem Zle_add_le_minus_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.
-now rewrite Zplus_simpl_r.
+now rewrite Zadd_simpl_r.
 Qed.
 
-Theorem Zlt_plus_lt_minus_l : forall n m p : Z, n + p < m <-> p < m - n.
+Theorem Zlt_add_lt_minus_l : forall n m p : Z, n + p < m <-> p < m - n.
 Proof.
-intros n m p. rewrite Zplus_comm; apply Zlt_plus_lt_minus_r.
+intros n m p. rewrite Zadd_comm; apply Zlt_add_lt_minus_r.
 Qed.
 
-Theorem Zle_plus_le_minus_l : forall n m p : Z, n + p <= m <-> p <= m - n.
+Theorem Zle_add_le_minus_l : forall n m p : Z, n + p <= m <-> p <= m - n.
 Proof.
-intros n m p. rewrite Zplus_comm; apply Zle_plus_le_minus_r.
+intros n m p. rewrite Zadd_comm; apply Zle_add_le_minus_r.
 Qed.
 
-Theorem Zlt_minus_lt_plus_r : forall n m p : Z, n - p < m <-> n < m + p.
+Theorem Zlt_minus_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 Zplus_lt_mono_r.
+intros n m p. stepl (n - p + p < m + p) by symmetry; apply Zadd_lt_mono_r.
 now rewrite Zminus_simpl_r.
 Qed.
 
-Theorem Zle_minus_le_plus_r : forall n m p : Z, n - p <= m <-> n <= m + p.
+Theorem Zle_minus_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 Zplus_le_mono_r.
+intros n m p. stepl (n - p + p <= m + p) by symmetry; apply Zadd_le_mono_r.
 now rewrite Zminus_simpl_r.
 Qed.
 
-Theorem Zlt_minus_lt_plus_l : forall n m p : Z, n - m < p <-> n < m + p.
+Theorem Zlt_minus_lt_add_l : forall n m p : Z, n - m < p <-> n < m + p.
 Proof.
-intros n m p. rewrite Zplus_comm; apply Zlt_minus_lt_plus_r.
+intros n m p. rewrite Zadd_comm; apply Zlt_minus_lt_add_r.
 Qed.
 
-Theorem Zle_minus_le_plus_l : forall n m p : Z, n - m <= p <-> n <= m + p.
+Theorem Zle_minus_le_add_l : forall n m p : Z, n - m <= p <-> n <= m + p.
 Proof.
-intros n m p. rewrite Zplus_comm; apply Zle_minus_le_plus_r.
+intros n m p. rewrite Zadd_comm; apply Zle_minus_le_add_r.
 Qed.
 
-Theorem Zlt_minus_lt_plus : forall n m p q : Z, n - m < p - q <-> n + q < m + p.
+Theorem Zlt_minus_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_plus_l. rewrite Zplus_minus_assoc.
-now rewrite <- Zlt_plus_lt_minus_r.
+intros n m p q. rewrite Zlt_minus_lt_add_l. rewrite Zadd_minus_assoc.
+now rewrite <- Zlt_add_lt_minus_r.
 Qed.
 
-Theorem Zle_minus_le_plus : forall n m p q : Z, n - m <= p - q <-> n + q <= m + p.
+Theorem Zle_minus_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_plus_l. rewrite Zplus_minus_assoc.
-now rewrite <- Zle_plus_le_minus_r.
+intros n m p q. rewrite Zle_minus_le_add_l. rewrite Zadd_minus_assoc.
+now rewrite <- Zle_add_le_minus_r.
 Qed.
 
 Theorem Zlt_minus_pos : forall n m : Z, 0 < m <-> n - m < n.
@@ -311,40 +311,40 @@ Qed.
 
 Theorem Zminus_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_plus in H. now apply Zplus_lt_cases.
+intros n m p q H. rewrite Zlt_minus_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.
 Proof.
-intros n m p q H. rewrite Zle_minus_le_plus in H. now apply Zplus_le_cases.
+intros n m p q H. rewrite Zle_minus_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.
 Proof.
-intros n m H; rewrite <- Zplus_opp_r in H.
+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 Zplus_neg_cases.
+now apply Zadd_neg_cases.
 Qed.
 
 Theorem Zminus_pos_cases : forall n m : Z, 0 < n - m -> 0 < n \/ m < 0.
 Proof.
-intros n m H; rewrite <- Zplus_opp_r in H.
+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 Zplus_pos_cases.
+now apply Zadd_pos_cases.
 Qed.
 
 Theorem Zminus_nonpos_cases : forall n m : Z, n - m <= 0 -> n <= 0 \/ 0 <= m.
 Proof.
-intros n m H; rewrite <- Zplus_opp_r in H.
+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 Zplus_nonpos_cases.
+now apply Zadd_nonpos_cases.
 Qed.
 
 Theorem Zminus_nonneg_cases : forall n m : Z, 0 <= n - m -> 0 <= n \/ m <= 0.
 Proof.
-intros n m H; rewrite <- Zplus_opp_r in H.
+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).
-now apply Zplus_nonneg_cases.
+now apply Zadd_nonneg_cases.
 Qed.
 
 Section PosNeg.
diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v
index 2d7ff30f7..ccf324a06 100644
--- a/theories/Numbers/Integer/Abstract/ZTimes.v
+++ b/theories/Numbers/Integer/Abstract/ZTimes.v
@@ -16,32 +16,32 @@ Module ZTimesPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZPlusPropMod := ZPlusPropFunct ZAxiomsMod.
 Open Local Scope IntScope.
 
-Theorem Ztimes_wd :
+Theorem Zmul_wd :
   forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 * m1 == n2 * m2.
-Proof NZtimes_wd.
+Proof NZmul_wd.
 
-Theorem Ztimes_0_l : forall n : Z, 0 * n == 0.
-Proof NZtimes_0_l.
+Theorem Zmul_0_l : forall n : Z, 0 * n == 0.
+Proof NZmul_0_l.
 
-Theorem Ztimes_succ_l : forall n m : Z, (S n) * m == n * m + m.
-Proof NZtimes_succ_l.
+Theorem Zmul_succ_l : forall n m : Z, (S n) * m == n * m + m.
+Proof NZmul_succ_l.
 
 (* Theorems that are valid for both natural numbers and integers *)
 
-Theorem Ztimes_0_r : forall n : Z, n * 0 == 0.
-Proof NZtimes_0_r.
+Theorem Zmul_0_r : forall n : Z, n * 0 == 0.
+Proof NZmul_0_r.
 
-Theorem Ztimes_succ_r : forall n m : Z, n * (S m) == n * m + n.
-Proof NZtimes_succ_r.
+Theorem Zmul_succ_r : forall n m : Z, n * (S m) == n * m + n.
+Proof NZmul_succ_r.
 
-Theorem Ztimes_comm : forall n m : Z, n * m == m * n.
-Proof NZtimes_comm.
+Theorem Zmul_comm : forall n m : Z, n * m == m * n.
+Proof NZmul_comm.
 
-Theorem Ztimes_plus_distr_r : forall n m p : Z, (n + m) * p == n * p + m * p.
-Proof NZtimes_plus_distr_r.
+Theorem Zmul_add_distr_r : forall n m p : Z, (n + m) * p == n * p + m * p.
+Proof NZmul_add_distr_r.
 
-Theorem Ztimes_plus_distr_l : forall n m p : Z, n * (m + p) == n * m + n * p.
-Proof NZtimes_plus_distr_l.
+Theorem Zmul_add_distr_l : forall n m p : Z, n * (m + p) == n * m + n * p.
+Proof NZmul_add_distr_l.
 
 (* A note on naming: right (correspondingly, left) distributivity happens
 when the sum is multiplied by a number on the right (left), not when the
@@ -50,64 +50,64 @@ and mathworld.wolfram.com). In the old library BinInt, distributivity over
 subtraction was named correctly, but distributivity over addition was named
 incorrectly. The names in Isabelle/HOL library are also incorrect. *)
 
-Theorem Ztimes_assoc : forall n m p : Z, n * (m * p) == (n * m) * p.
-Proof NZtimes_assoc.
+Theorem Zmul_assoc : forall n m p : Z, n * (m * p) == (n * m) * p.
+Proof NZmul_assoc.
 
-Theorem Ztimes_1_l : forall n : Z, 1 * n == n.
-Proof NZtimes_1_l.
+Theorem Zmul_1_l : forall n : Z, 1 * n == n.
+Proof NZmul_1_l.
 
-Theorem Ztimes_1_r : forall n : Z, n * 1 == n.
-Proof NZtimes_1_r.
+Theorem Zmul_1_r : forall n : Z, n * 1 == n.
+Proof NZmul_1_r.
 
 (* The following two theorems are true in an ordered ring,
 but since they don't mention order, we'll put them here *)
 
-Theorem Zeq_times_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0.
-Proof NZeq_times_0.
+Theorem Zeq_mul_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0.
+Proof NZeq_mul_0.
 
-Theorem Zneq_times_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
-Proof NZneq_times_0.
+Theorem Zneq_mul_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
+Proof NZneq_mul_0.
 
 (* Theorems that are either not valid on N or have different proofs on N and Z *)
 
-Theorem Ztimes_pred_r : forall n m : Z, n * (P m) == n * m - n.
+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 Ztimes_succ_r, <- Zplus_minus_assoc, Zminus_diag, Zplus_0_r.
+now rewrite Zmul_succ_r, <- Zadd_minus_assoc, Zminus_diag, Zadd_0_r.
 Qed.
 
-Theorem Ztimes_pred_l : forall n m : Z, (P n) * m == n * m - m.
+Theorem Zmul_pred_l : forall n m : Z, (P n) * m == n * m - m.
 Proof.
-intros n m; rewrite (Ztimes_comm (P n) m), (Ztimes_comm n m). apply Ztimes_pred_r.
+intros n m; rewrite (Zmul_comm (P n) m), (Zmul_comm n m). apply Zmul_pred_r.
 Qed.
 
-Theorem Ztimes_opp_l : forall n m : Z, (- n) * m == - (n * m).
+Theorem Zmul_opp_l : forall n m : Z, (- n) * m == - (n * m).
 Proof.
-intros n m. apply -> Zplus_move_0_r.
-now rewrite <- Ztimes_plus_distr_r, Zplus_opp_diag_l, Ztimes_0_l.
+intros n m. apply -> Zadd_move_0_r.
+now rewrite <- Zmul_add_distr_r, Zadd_opp_diag_l, Zmul_0_l.
 Qed.
 
-Theorem Ztimes_opp_r : forall n m : Z, n * (- m) == - (n * m).
+Theorem Zmul_opp_r : forall n m : Z, n * (- m) == - (n * m).
 Proof.
-intros n m; rewrite (Ztimes_comm n (- m)), (Ztimes_comm n m); apply Ztimes_opp_l.
+intros n m; rewrite (Zmul_comm n (- m)), (Zmul_comm n m); apply Zmul_opp_l.
 Qed.
 
-Theorem Ztimes_opp_opp : forall n m : Z, (- n) * (- m) == n * m.
+Theorem Zmul_opp_opp : forall n m : Z, (- n) * (- m) == n * m.
 Proof.
-intros n m; now rewrite Ztimes_opp_l, Ztimes_opp_r, Zopp_involutive.
+intros n m; now rewrite Zmul_opp_l, Zmul_opp_r, Zopp_involutive.
 Qed.
 
-Theorem Ztimes_minus_distr_l : forall n m p : Z, n * (m - p) == n * m - n * p.
+Theorem Zmul_minus_distr_l : forall n m p : Z, n * (m - p) == n * m - n * p.
 Proof.
-intros n m p. do 2 rewrite <- Zplus_opp_r. rewrite Ztimes_plus_distr_l.
-now rewrite Ztimes_opp_r.
+intros n m p. do 2 rewrite <- Zadd_opp_r. rewrite Zmul_add_distr_l.
+now rewrite Zmul_opp_r.
 Qed.
 
-Theorem Ztimes_minus_distr_r : forall n m p : Z, (n - m) * p == n * p - m * p.
+Theorem Zmul_minus_distr_r : forall n m p : Z, (n - m) * p == n * p - m * p.
 Proof.
-intros n m p; rewrite (Ztimes_comm (n - m) p), (Ztimes_comm n p), (Ztimes_comm m p);
-now apply Ztimes_minus_distr_l.
+intros n m p; rewrite (Zmul_comm (n - m) p), (Zmul_comm n p), (Zmul_comm m p);
+now apply Zmul_minus_distr_l.
 Qed.
 
 End ZTimesPropFunct.
diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
index 6b6f34d75..d3f5a0396 100644
--- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
@@ -16,187 +16,187 @@ Module ZTimesOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZPlusOrderPropMod := ZPlusOrderPropFunct ZAxiomsMod.
 Open Local Scope IntScope.
 
-Theorem Ztimes_lt_pred :
+Theorem Zmul_lt_pred :
   forall p q n m : Z, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
-Proof NZtimes_lt_pred.
+Proof NZmul_lt_pred.
 
-Theorem Ztimes_lt_mono_pos_l : forall p n m : Z, 0 < p -> (n < m <-> p * n < p * m).
-Proof NZtimes_lt_mono_pos_l.
+Theorem Zmul_lt_mono_pos_l : forall p n m : Z, 0 < p -> (n < m <-> p * n < p * m).
+Proof NZmul_lt_mono_pos_l.
 
-Theorem Ztimes_lt_mono_pos_r : forall p n m : Z, 0 < p -> (n < m <-> n * p < m * p).
-Proof NZtimes_lt_mono_pos_r.
+Theorem Zmul_lt_mono_pos_r : forall p n m : Z, 0 < p -> (n < m <-> n * p < m * p).
+Proof NZmul_lt_mono_pos_r.
 
-Theorem Ztimes_lt_mono_neg_l : forall p n m : Z, p < 0 -> (n < m <-> p * m < p * n).
-Proof NZtimes_lt_mono_neg_l.
+Theorem Zmul_lt_mono_neg_l : forall p n m : Z, p < 0 -> (n < m <-> p * m < p * n).
+Proof NZmul_lt_mono_neg_l.
 
-Theorem Ztimes_lt_mono_neg_r : forall p n m : Z, p < 0 -> (n < m <-> m * p < n * p).
-Proof NZtimes_lt_mono_neg_r.
+Theorem Zmul_lt_mono_neg_r : forall p n m : Z, p < 0 -> (n < m <-> m * p < n * p).
+Proof NZmul_lt_mono_neg_r.
 
-Theorem Ztimes_le_mono_nonneg_l : forall n m p : Z, 0 <= p -> n <= m -> p * n <= p * m.
-Proof NZtimes_le_mono_nonneg_l.
+Theorem Zmul_le_mono_nonneg_l : forall n m p : Z, 0 <= p -> n <= m -> p * n <= p * m.
+Proof NZmul_le_mono_nonneg_l.
 
-Theorem Ztimes_le_mono_nonpos_l : forall n m p : Z, p <= 0 -> n <= m -> p * m <= p * n.
-Proof NZtimes_le_mono_nonpos_l.
+Theorem Zmul_le_mono_nonpos_l : forall n m p : Z, p <= 0 -> n <= m -> p * m <= p * n.
+Proof NZmul_le_mono_nonpos_l.
 
-Theorem Ztimes_le_mono_nonneg_r : forall n m p : Z, 0 <= p -> n <= m -> n * p <= m * p.
-Proof NZtimes_le_mono_nonneg_r.
+Theorem Zmul_le_mono_nonneg_r : forall n m p : Z, 0 <= p -> n <= m -> n * p <= m * p.
+Proof NZmul_le_mono_nonneg_r.
 
-Theorem Ztimes_le_mono_nonpos_r : forall n m p : Z, p <= 0 -> n <= m -> m * p <= n * p.
-Proof NZtimes_le_mono_nonpos_r.
+Theorem Zmul_le_mono_nonpos_r : forall n m p : Z, p <= 0 -> n <= m -> m * p <= n * p.
+Proof NZmul_le_mono_nonpos_r.
 
-Theorem Ztimes_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m).
-Proof NZtimes_cancel_l.
+Theorem Zmul_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m).
+Proof NZmul_cancel_l.
 
-Theorem Ztimes_cancel_r : forall n m p : Z, p ~= 0 -> (n * p == m * p <-> n == m).
-Proof NZtimes_cancel_r.
+Theorem Zmul_cancel_r : forall n m p : Z, p ~= 0 -> (n * p == m * p <-> n == m).
+Proof NZmul_cancel_r.
 
-Theorem Ztimes_id_l : forall n m : Z, m ~= 0 -> (n * m == m <-> n == 1).
-Proof NZtimes_id_l.
+Theorem Zmul_id_l : forall n m : Z, m ~= 0 -> (n * m == m <-> n == 1).
+Proof NZmul_id_l.
 
-Theorem Ztimes_id_r : forall n m : Z, n ~= 0 -> (n * m == n <-> m == 1).
-Proof NZtimes_id_r.
+Theorem Zmul_id_r : forall n m : Z, n ~= 0 -> (n * m == n <-> m == 1).
+Proof NZmul_id_r.
 
-Theorem Ztimes_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m).
-Proof NZtimes_le_mono_pos_l.
+Theorem Zmul_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m).
+Proof NZmul_le_mono_pos_l.
 
-Theorem Ztimes_le_mono_pos_r : forall n m p : Z, 0 < p -> (n <= m <-> n * p <= m * p).
-Proof NZtimes_le_mono_pos_r.
+Theorem Zmul_le_mono_pos_r : forall n m p : Z, 0 < p -> (n <= m <-> n * p <= m * p).
+Proof NZmul_le_mono_pos_r.
 
-Theorem Ztimes_le_mono_neg_l : forall n m p : Z, p < 0 -> (n <= m <-> p * m <= p * n).
-Proof NZtimes_le_mono_neg_l.
+Theorem Zmul_le_mono_neg_l : forall n m p : Z, p < 0 -> (n <= m <-> p * m <= p * n).
+Proof NZmul_le_mono_neg_l.
 
-Theorem Ztimes_le_mono_neg_r : forall n m p : Z, p < 0 -> (n <= m <-> m * p <= n * p).
-Proof NZtimes_le_mono_neg_r.
+Theorem Zmul_le_mono_neg_r : forall n m p : Z, p < 0 -> (n <= m <-> m * p <= n * p).
+Proof NZmul_le_mono_neg_r.
 
-Theorem Ztimes_lt_mono_nonneg :
+Theorem Zmul_lt_mono_nonneg :
   forall n m p q : Z, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q.
-Proof NZtimes_lt_mono_nonneg.
+Proof NZmul_lt_mono_nonneg.
 
-Theorem Ztimes_lt_mono_nonpos :
+Theorem Zmul_lt_mono_nonpos :
   forall n m p q : Z, m <= 0 -> n < m -> q <= 0 -> p < q ->  m * q < n * p.
 Proof.
 intros n m p q H1 H2 H3 H4.
 apply Zle_lt_trans with (m * p).
-apply Ztimes_le_mono_nonpos_l; [assumption | now apply Zlt_le_incl].
-apply -> Ztimes_lt_mono_neg_r; [assumption | now apply Zlt_le_trans with q].
+apply Zmul_le_mono_nonpos_l; [assumption | now apply Zlt_le_incl].
+apply -> Zmul_lt_mono_neg_r; [assumption | now apply Zlt_le_trans with q].
 Qed.
 
-Theorem Ztimes_le_mono_nonneg :
+Theorem Zmul_le_mono_nonneg :
   forall n m p q : Z, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q.
-Proof NZtimes_le_mono_nonneg.
+Proof NZmul_le_mono_nonneg.
 
-Theorem Ztimes_le_mono_nonpos :
+Theorem Zmul_le_mono_nonpos :
   forall n m p q : Z, m <= 0 -> n <= m -> q <= 0 -> p <= q ->  m * q <= n * p.
 Proof.
 intros n m p q H1 H2 H3 H4.
 apply Zle_trans with (m * p).
-now apply Ztimes_le_mono_nonpos_l.
-apply Ztimes_le_mono_nonpos_r; [now apply Zle_trans with q | assumption].
+now apply Zmul_le_mono_nonpos_l.
+apply Zmul_le_mono_nonpos_r; [now apply Zle_trans with q | assumption].
 Qed.
 
-Theorem Ztimes_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n * m.
-Proof NZtimes_pos_pos.
+Theorem Zmul_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n * m.
+Proof NZmul_pos_pos.
 
-Theorem Ztimes_neg_neg : forall n m : Z, n < 0 -> m < 0 -> 0 < n * m.
-Proof NZtimes_neg_neg.
+Theorem Zmul_neg_neg : forall n m : Z, n < 0 -> m < 0 -> 0 < n * m.
+Proof NZmul_neg_neg.
 
-Theorem Ztimes_pos_neg : forall n m : Z, 0 < n -> m < 0 -> n * m < 0.
-Proof NZtimes_pos_neg.
+Theorem Zmul_pos_neg : forall n m : Z, 0 < n -> m < 0 -> n * m < 0.
+Proof NZmul_pos_neg.
 
-Theorem Ztimes_neg_pos : forall n m : Z, n < 0 -> 0 < m -> n * m < 0.
-Proof NZtimes_neg_pos.
+Theorem Zmul_neg_pos : forall n m : Z, n < 0 -> 0 < m -> n * m < 0.
+Proof NZmul_neg_pos.
 
-Theorem Ztimes_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m.
+Theorem Zmul_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m.
 Proof.
 intros n m H1 H2.
-rewrite <- (Ztimes_0_l m). now apply Ztimes_le_mono_nonneg_r.
+rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonneg_r.
 Qed.
 
-Theorem Ztimes_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m.
+Theorem Zmul_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m.
 Proof.
 intros n m H1 H2.
-rewrite <- (Ztimes_0_l m). now apply Ztimes_le_mono_nonpos_r.
+rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonpos_r.
 Qed.
 
-Theorem Ztimes_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0.
+Theorem Zmul_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0.
 Proof.
 intros n m H1 H2.
-rewrite <- (Ztimes_0_l m). now apply Ztimes_le_mono_nonpos_r.
+rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonpos_r.
 Qed.
 
-Theorem Ztimes_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0.
+Theorem Zmul_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0.
 Proof.
-intros; rewrite Ztimes_comm; now apply Ztimes_nonneg_nonpos.
+intros; rewrite Zmul_comm; now apply Zmul_nonneg_nonpos.
 Qed.
 
-Theorem Zlt_1_times_pos : forall n m : Z, 1 < n -> 0 < m -> 1 < n * m.
-Proof NZlt_1_times_pos.
+Theorem Zlt_1_mul_pos : forall n m : Z, 1 < n -> 0 < m -> 1 < n * m.
+Proof NZlt_1_mul_pos.
 
-Theorem Zeq_times_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0.
-Proof NZeq_times_0.
+Theorem Zeq_mul_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0.
+Proof NZeq_mul_0.
 
-Theorem Zneq_times_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
-Proof NZneq_times_0.
+Theorem Zneq_mul_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
+Proof NZneq_mul_0.
 
 Theorem Zeq_square_0 : forall n : Z, n * n == 0 <-> n == 0.
 Proof NZeq_square_0.
 
-Theorem Zeq_times_0_l : forall n m : Z, n * m == 0 -> m ~= 0 -> n == 0.
-Proof NZeq_times_0_l.
+Theorem Zeq_mul_0_l : forall n m : Z, n * m == 0 -> m ~= 0 -> n == 0.
+Proof NZeq_mul_0_l.
 
-Theorem Zeq_times_0_r : forall n m : Z, n * m == 0 -> n ~= 0 -> m == 0.
-Proof NZeq_times_0_r.
+Theorem Zeq_mul_0_r : forall n m : Z, n * m == 0 -> n ~= 0 -> m == 0.
+Proof NZeq_mul_0_r.
 
-Theorem Zlt_0_times : forall n m : Z, 0 < n * m <-> 0 < n /\ 0 < m \/ m < 0 /\ n < 0.
-Proof NZlt_0_times.
+Theorem Zlt_0_mul : forall n m : Z, 0 < n * m <-> 0 < n /\ 0 < m \/ m < 0 /\ n < 0.
+Proof NZlt_0_mul.
 
-Notation Ztimes_pos := Zlt_0_times (only parsing).
+Notation Zmul_pos := Zlt_0_mul (only parsing).
 
-Theorem Zlt_times_0 :
+Theorem Zlt_mul_0 :
   forall n m : Z, n * m < 0 <-> n < 0 /\ m > 0 \/ n > 0 /\ m < 0.
 Proof.
 intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]].
 destruct (Zlt_trichotomy n 0) as [H1 | [H1 | H1]];
-[| rewrite H1 in H; rewrite Ztimes_0_l in H; false_hyp H Zlt_irrefl |];
+[| rewrite H1 in H; rewrite Zmul_0_l in H; false_hyp H Zlt_irrefl |];
 (destruct (Zlt_trichotomy m 0) as [H2 | [H2 | H2]];
-[| rewrite H2 in H; rewrite Ztimes_0_r in H; false_hyp H Zlt_irrefl |]);
+[| rewrite H2 in H; rewrite Zmul_0_r in H; false_hyp H Zlt_irrefl |]);
 try (left; now split); try (right; now split).
-assert (H3 : n * m > 0) by now apply Ztimes_neg_neg.
+assert (H3 : n * m > 0) by now apply Zmul_neg_neg.
 elimtype False; now apply (Zlt_asymm (n * m) 0).
-assert (H3 : n * m > 0) by now apply Ztimes_pos_pos.
+assert (H3 : n * m > 0) by now apply Zmul_pos_pos.
 elimtype False; now apply (Zlt_asymm (n * m) 0).
-now apply Ztimes_neg_pos. now apply Ztimes_pos_neg.
+now apply Zmul_neg_pos. now apply Zmul_pos_neg.
 Qed.
 
-Notation Ztimes_neg := Zlt_times_0 (only parsing).
+Notation Zmul_neg := Zlt_mul_0 (only parsing).
 
-Theorem Zle_0_times :
+Theorem Zle_0_mul :
   forall n m : Z, 0 <= n * m -> 0 <= n /\ 0 <= m \/ n <= 0 /\ m <= 0.
 Proof.
 assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_symm).
 intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R.
-rewrite Zlt_0_times, Zeq_times_0.
+rewrite Zlt_0_mul, Zeq_mul_0.
 pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto.
 Qed.
 
-Notation Ztimes_nonneg := Zle_0_times (only parsing).
+Notation Zmul_nonneg := Zle_0_mul (only parsing).
 
-Theorem Zle_times_0 :
+Theorem Zle_mul_0 :
   forall n m : Z, n * m <= 0 -> 0 <= n /\ m <= 0 \/ n <= 0 /\ 0 <= m.
 Proof.
 assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_symm).
 intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R.
-rewrite Zlt_times_0, Zeq_times_0.
+rewrite Zlt_mul_0, Zeq_mul_0.
 pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto.
 Qed.
 
-Notation Ztimes_nonpos := Zle_times_0 (only parsing).
+Notation Zmul_nonpos := Zle_mul_0 (only parsing).
 
 Theorem Zle_0_square : forall n : Z, 0 <= n * n.
 Proof.
 intro n; destruct (Zneg_nonneg_cases n).
-apply Zlt_le_incl; now apply Ztimes_neg_neg.
-now apply Ztimes_nonneg_nonneg.
+apply Zlt_le_incl; now apply Zmul_neg_neg.
+now apply Zmul_nonneg_nonneg.
 Qed.
 
 Notation Zsquare_nonneg := Zle_0_square (only parsing).
@@ -211,7 +211,7 @@ Proof NZsquare_lt_mono_nonneg.
 
 Theorem Zsquare_lt_mono_nonpos : forall n m : Z, n <= 0 -> m < n -> n * n < m * m.
 Proof.
-intros n m H1 H2. now apply Ztimes_lt_mono_nonpos.
+intros n m H1 H2. now apply Zmul_lt_mono_nonpos.
 Qed.
 
 Theorem Zsquare_le_mono_nonneg : forall n m : Z, 0 <= n -> n <= m -> n * n <= m * m.
@@ -219,7 +219,7 @@ Proof NZsquare_le_mono_nonneg.
 
 Theorem Zsquare_le_mono_nonpos : forall n m : Z, n <= 0 -> m <= n -> n * n <= m * m.
 Proof.
-intros n m H1 H2. now apply Ztimes_le_mono_nonpos.
+intros n m H1 H2. now apply Zmul_le_mono_nonpos.
 Qed.
 
 Theorem Zsquare_lt_simpl_nonneg : forall n m : Z, 0 <= m -> n * n < m * m -> n < m.
@@ -246,96 +246,96 @@ apply -> NZlt_nge in F. false_hyp H2 F.
 apply Zlt_le_incl; now apply NZle_lt_trans with 0.
 Qed.
 
-Theorem Ztimes_2_mono_l : forall n m : Z, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
-Proof NZtimes_2_mono_l.
+Theorem Zmul_2_mono_l : forall n m : Z, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
+Proof NZmul_2_mono_l.
 
-Theorem Zlt_1_times_neg : forall n m : Z, n < -1 -> m < 0 -> 1 < n * m.
+Theorem Zlt_1_mul_neg : forall n m : Z, n < -1 -> m < 0 -> 1 < n * m.
 Proof.
-intros n m H1 H2. apply -> (NZtimes_lt_mono_neg_r m) in H1.
-apply <- Zopp_pos_neg in H2. rewrite Ztimes_opp_l, Ztimes_1_l in H1.
+intros n m H1 H2. apply -> (NZmul_lt_mono_neg_r m) in H1.
+apply <- Zopp_pos_neg in H2. rewrite Zmul_opp_l, Zmul_1_l in H1.
 now apply Zlt_1_l with (- m).
 assumption.
 Qed.
 
-Theorem Zlt_times_n1_neg : forall n m : Z, 1 < n -> m < 0 -> n * m < -1.
+Theorem Zlt_mul_n1_neg : forall n m : Z, 1 < n -> m < 0 -> n * m < -1.
 Proof.
-intros n m H1 H2. apply -> (NZtimes_lt_mono_neg_r m) in H1.
-rewrite Ztimes_1_l in H1. now apply Zlt_n1_r with m.
+intros n m H1 H2. apply -> (NZmul_lt_mono_neg_r m) in H1.
+rewrite Zmul_1_l in H1. now apply Zlt_n1_r with m.
 assumption.
 Qed.
 
-Theorem Zlt_times_n1_pos : forall n m : Z, n < -1 -> 0 < m -> n * m < -1.
+Theorem Zlt_mul_n1_pos : forall n m : Z, n < -1 -> 0 < m -> n * m < -1.
 Proof.
-intros n m H1 H2. apply -> (NZtimes_lt_mono_pos_r m) in H1.
-rewrite Ztimes_opp_l, Ztimes_1_l in H1.
+intros n m H1 H2. apply -> (NZmul_lt_mono_pos_r m) in H1.
+rewrite Zmul_opp_l, Zmul_1_l in H1.
 apply <- Zopp_neg_pos in H2. now apply Zlt_n1_r with (- m).
 assumption.
 Qed.
 
-Theorem Zlt_1_times_l : forall n m : Z, 1 < n -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
+Theorem Zlt_1_mul_l : forall n m : Z, 1 < n -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
 Proof.
 intros n m H; destruct (Zlt_trichotomy m 0) as [H1 | [H1 | H1]].
-left. now apply Zlt_times_n1_neg.
-right; left; now rewrite H1, Ztimes_0_r.
-right; right; now apply Zlt_1_times_pos.
+left. now apply Zlt_mul_n1_neg.
+right; left; now rewrite H1, Zmul_0_r.
+right; right; now apply Zlt_1_mul_pos.
 Qed.
 
-Theorem Zlt_n1_times_r : forall n m : Z, n < -1 -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
+Theorem Zlt_n1_mul_r : forall n m : Z, n < -1 -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
 Proof.
 intros n m H; destruct (Zlt_trichotomy m 0) as [H1 | [H1 | H1]].
-right; right. now apply Zlt_1_times_neg.
-right; left; now rewrite H1, Ztimes_0_r.
-left. now apply Zlt_times_n1_pos.
+right; right. now apply Zlt_1_mul_neg.
+right; left; now rewrite H1, Zmul_0_r.
+left. now apply Zlt_mul_n1_pos.
 Qed.
 
-Theorem Zeq_times_1 : forall n m : Z, n * m == 1 -> n == 1 \/ n == -1.
+Theorem Zeq_mul_1 : forall n m : Z, n * m == 1 -> n == 1 \/ n == -1.
 Proof.
 assert (F : ~ 1 < -1).
 intro H.
 assert (H1 : -1 < 0). apply <- Zopp_neg_pos. apply Zlt_succ_diag_r.
 assert (H2 : 1 < 0) by now apply Zlt_trans with (-1). false_hyp H2 Znlt_succ_diag_l.
 Z0_pos_neg n.
-intros m H; rewrite Ztimes_0_l in H; false_hyp H Zneq_succ_diag_r.
+intros m H; rewrite Zmul_0_l in H; false_hyp H Zneq_succ_diag_r.
 intros n H; split; apply <- Zle_succ_l in H; le_elim H.
-intros m H1; apply (Zlt_1_times_l n m) in H.
+intros m H1; apply (Zlt_1_mul_l n m) in H.
 rewrite H1 in H; destruct H as [H | [H | H]].
 false_hyp H F. false_hyp H Zneq_succ_diag_l. false_hyp H Zlt_irrefl.
 intros; now left.
-intros m H1; apply (Zlt_1_times_l n m) in H. rewrite Ztimes_opp_l in H1;
+intros m H1; apply (Zlt_1_mul_l n m) in H. rewrite Zmul_opp_l in H1;
 apply -> Zeq_opp_l in H1. rewrite H1 in H; destruct H as [H | [H | H]].
 false_hyp H Zlt_irrefl. apply -> Zeq_opp_l in H. rewrite Zopp_0 in H.
 false_hyp H Zneq_succ_diag_l. false_hyp H F.
 intros; right; symmetry; now apply Zopp_wd.
 Qed.
 
-Theorem Zlt_times_diag_l : forall n m : Z, n < 0 -> (1 < m <-> n * m < n).
+Theorem Zlt_mul_diag_l : forall n m : Z, n < 0 -> (1 < m <-> n * m < n).
 Proof.
-intros n m H. stepr (n * m < n * 1) by now rewrite Ztimes_1_r.
-now apply Ztimes_lt_mono_neg_l.
+intros n m H. stepr (n * m < n * 1) by now rewrite Zmul_1_r.
+now apply Zmul_lt_mono_neg_l.
 Qed.
 
-Theorem Zlt_times_diag_r : forall n m : Z, 0 < n -> (1 < m <-> n < n * m).
+Theorem Zlt_mul_diag_r : forall n m : Z, 0 < n -> (1 < m <-> n < n * m).
 Proof.
-intros n m H. stepr (n * 1 < n * m) by now rewrite Ztimes_1_r.
-now apply Ztimes_lt_mono_pos_l.
+intros n m H. stepr (n * 1 < n * m) by now rewrite Zmul_1_r.
+now apply Zmul_lt_mono_pos_l.
 Qed.
 
-Theorem Zle_times_diag_l : forall n m : Z, n < 0 -> (1 <= m <-> n * m <= n).
+Theorem Zle_mul_diag_l : forall n m : Z, n < 0 -> (1 <= m <-> n * m <= n).
 Proof.
-intros n m H. stepr (n * m <= n * 1) by now rewrite Ztimes_1_r.
-now apply Ztimes_le_mono_neg_l.
+intros n m H. stepr (n * m <= n * 1) by now rewrite Zmul_1_r.
+now apply Zmul_le_mono_neg_l.
 Qed.
 
-Theorem Zle_times_diag_r : forall n m : Z, 0 < n -> (1 <= m <-> n <= n * m).
+Theorem Zle_mul_diag_r : forall n m : Z, 0 < n -> (1 <= m <-> n <= n * m).
 Proof.
-intros n m H. stepr (n * 1 <= n * m) by now rewrite Ztimes_1_r.
-now apply Ztimes_le_mono_pos_l.
+intros n m H. stepr (n * 1 <= n * m) by now rewrite Zmul_1_r.
+now apply Zmul_le_mono_pos_l.
 Qed.
 
-Theorem Zlt_times_r : forall n m p : Z, 0 < n -> 1 < p -> n < m -> n < m * p.
+Theorem Zlt_mul_r : forall n m p : Z, 0 < n -> 1 < p -> n < m -> n < m * p.
 Proof.
-intros. stepl (n * 1) by now rewrite Ztimes_1_r.
-apply Ztimes_lt_mono_nonneg.
+intros. stepl (n * 1) by now rewrite Zmul_1_r.
+apply Zmul_lt_mono_nonneg.
 now apply Zlt_le_incl. assumption. apply Zle_0_1. assumption.
 Qed.
 
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index d2f9b0a02..f54737036 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -80,7 +80,7 @@ Proof.
 red; intros; zsimpl; auto.
 Qed.
 
-Lemma plus_opp : forall x : bigZ, x + (- x) == 0.
+Lemma add_opp : forall x : bigZ, x + (- x) == 0.
 Proof.
 red; intros; zsimpl; auto with zarith.
 Qed.
@@ -91,15 +91,15 @@ Lemma BigZring :
  ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq.
 Proof.
 constructor.
-exact Zplus_0_l.
-exact Zplus_comm.
-exact Zplus_assoc.
-exact Ztimes_1_l.
-exact Ztimes_comm.
-exact Ztimes_assoc.
-exact Ztimes_plus_distr_r.
+exact Zadd_0_l.
+exact Zadd_comm.
+exact Zadd_assoc.
+exact Zmul_1_l.
+exact Zmul_comm.
+exact Zmul_assoc.
+exact Zmul_add_distr_r.
 exact sub_opp.
-exact plus_opp.
+exact add_opp.
 Qed.
 
 Add Ring BigZr : BigZring.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 1df0a7833..acc77b3e7 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 Require Import ZTimesOrder.
 Require Import ZArith.
@@ -24,9 +24,9 @@ Definition NZeq := (@eq Z).
 Definition NZ0 := 0.
 Definition NZsucc := Zsucc'.
 Definition NZpred := Zpred'.
-Definition NZplus := Zplus.
+Definition NZadd := Zplus.
 Definition NZminus := Zminus.
-Definition NZtimes := Zmult.
+Definition NZmul := Zmult.
 
 Theorem NZeq_equiv : equiv Z NZeq.
 Proof.
@@ -49,7 +49,7 @@ Proof.
 congruence.
 Qed.
 
-Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd.
+Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.
 Proof.
 congruence.
 Qed.
@@ -59,7 +59,7 @@ Proof.
 congruence.
 Qed.
 
-Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd.
+Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.
 Proof.
 congruence.
 Qed.
@@ -79,12 +79,12 @@ intros; now apply -> AS.
 intros n H. rewrite <- (Zsucc'_pred' n) in H. now apply <- AS.
 Qed.
 
-Theorem NZplus_0_l : forall n : Z, 0 + n = n.
+Theorem NZadd_0_l : forall n : Z, 0 + n = n.
 Proof.
 exact Zplus_0_l.
 Qed.
 
-Theorem NZplus_succ_l : forall n m : Z, (NZsucc n) + m = NZsucc (n + m).
+Theorem NZadd_succ_l : forall n m : Z, (NZsucc n) + m = NZsucc (n + m).
 Proof.
 intros; do 2 rewrite <- Zsucc_succ'; apply Zplus_succ_l.
 Qed.
@@ -100,12 +100,12 @@ intros; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred';
 apply Zminus_succ_r.
 Qed.
 
-Theorem NZtimes_0_l : forall n : Z, 0 * n = 0.
+Theorem NZmul_0_l : forall n : Z, 0 * n = 0.
 Proof.
 reflexivity.
 Qed.
 
-Theorem NZtimes_succ_l : forall n m : Z, (NZsucc n) * m = n * m + m.
+Theorem NZmul_succ_l : forall n m : Z, (NZsucc n) * m = n * m + m.
 Proof.
 intros; rewrite <- Zsucc_succ'; apply Zmult_succ_l.
 Qed.
@@ -217,18 +217,18 @@ Module Export ZBinTimesOrderPropMod := ZTimesOrderPropFunct ZBinAxiomsMod.
 
 (** Z forms a ring *)
 
-(*Lemma Zring : ring_theory 0 1 NZplus NZtimes NZminus Zopp NZeq.
+(*Lemma Zring : ring_theory 0 1 NZadd NZmul NZminus Zopp NZeq.
 Proof.
 constructor.
-exact Zplus_0_l.
-exact Zplus_comm.
-exact Zplus_assoc.
-exact Ztimes_1_l.
-exact Ztimes_comm.
-exact Ztimes_assoc.
-exact Ztimes_plus_distr_r.
-intros; now rewrite Zplus_opp_minus.
-exact Zplus_opp_r.
+exact Zadd_0_l.
+exact Zadd_comm.
+exact Zadd_assoc.
+exact Zmul_1_l.
+exact Zmul_comm.
+exact Zmul_assoc.
+exact Zmul_add_distr_r.
+intros; now rewrite Zadd_opp_minus.
+exact Zadd_opp_r.
 Qed.
 
 Add Ring ZR : Zring.*)
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index facffef45..97a72e087 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -29,23 +29,23 @@ reasons we define an abstract semiring here. *)
 
 Open Local Scope NatScope.
 
-Lemma Nsemi_ring : semi_ring_theory 0 1 plus times Neq.
+Lemma Nsemi_ring : semi_ring_theory 0 1 add mul Neq.
 Proof.
 constructor.
-exact plus_0_l.
-exact plus_comm.
-exact plus_assoc.
-exact times_1_l.
-exact times_0_l.
-exact times_comm.
-exact times_assoc.
-exact times_plus_distr_r.
+exact add_0_l.
+exact add_comm.
+exact add_assoc.
+exact mul_1_l.
+exact mul_0_l.
+exact mul_comm.
+exact mul_assoc.
+exact mul_add_distr_r.
 Qed.
 
 Add Ring NSR : Nsemi_ring.
 
-(* The definitios of functions (NZplus, NZtimes, etc.) will be unfolded by
-the properties functor. Since we don't want Zplus_comm to refer to unfolded
+(* The definitios of functions (NZadd, NZmul, etc.) will be unfolded by
+the properties functor. Since we don't want Zadd_comm to refer to unfolded
 definitions of equality: fun p1 p2 : NZ => (fst p1 + snd p2) = (fst p2 + snd p1),
 we will provide an extra layer of definitions. *)
 
@@ -61,13 +61,13 @@ elements is 0, and make all operations convert canonical values into other
 canonical values. In that case, we could get rid of setoids and arrive at
 integers as signed natural numbers. *)
 
-Definition Zplus (n m : Z) : Z := ((fst n) + (fst m), (snd n) + (snd m)).
+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)).
 
 (* Unfortunately, the elements of the pair keep increasing, even during
 subtraction *)
 
-Definition Ztimes (n m : Z) : Z :=
+Definition Zmul (n m : Z) : Z :=
   ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)).
 Definition Zlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n).
 Definition Zle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n).
@@ -80,9 +80,9 @@ Notation "x == y"  := (Zeq x y) (at level 70) : IntScope.
 Notation "x ~= y" := (~ Zeq x y) (at level 70) : IntScope.
 Notation "0" := Z0 : IntScope.
 Notation "1" := (Zsucc Z0) : IntScope.
-Notation "x + y" := (Zplus x y) : IntScope.
+Notation "x + y" := (Zadd x y) : IntScope.
 Notation "x - y" := (Zminus x y) : IntScope.
-Notation "x * y" := (Ztimes x y) : IntScope.
+Notation "x * y" := (Zmul x y) : IntScope.
 Notation "x < y" := (Zlt x y) : IntScope.
 Notation "x <= y" := (Zle x y) : IntScope.
 Notation "x > y" := (Zlt y x) (only parsing) : IntScope.
@@ -91,7 +91,7 @@ Notation "x >= y" := (Zle y x) (only parsing) : IntScope.
 Notation Local N := NZ.
 (* To remember N without having to use a long qualifying name. since NZ will be redefined *)
 Notation Local NE := NZeq (only parsing).
-Notation Local plus_wd := NZplus_wd (only parsing).
+Notation Local add_wd := NZadd_wd (only parsing).
 
 Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
 Module Export NZAxiomsMod <: NZAxiomsSig.
@@ -101,9 +101,9 @@ Definition NZeq := Zeq.
 Definition NZ0 := Z0.
 Definition NZsucc := Zsucc.
 Definition NZpred := Zpred.
-Definition NZplus := Zplus.
+Definition NZadd := Zadd.
 Definition NZminus := Zminus.
-Definition NZtimes := Ztimes.
+Definition NZmul := Zmul.
 
 Theorem ZE_refl : reflexive Z Zeq.
 Proof.
@@ -119,10 +119,10 @@ Theorem ZE_trans : transitive Z Zeq.
 Proof.
 unfold transitive, Zeq. intros n m p H1 H2.
 assert (H3 : (fst n + snd m) + (fst m + snd p) == (fst m + snd n) + (fst p + snd m))
-by now apply plus_wd.
+by now apply add_wd.
 stepl ((fst n + snd p) + (fst m + snd m)) in H3 by ring.
 stepr ((fst p + snd n) + (fst m + snd m)) in H3 by ring.
-now apply -> plus_cancel_r in H3.
+now apply -> add_cancel_r in H3.
 Qed.
 
 Theorem NZeq_equiv : equiv Z Zeq.
@@ -144,20 +144,20 @@ Qed.
 Add Morphism NZsucc with signature Zeq ==> Zeq as NZsucc_wd.
 Proof.
 unfold NZsucc, Zeq; intros n m H; simpl.
-do 2 rewrite plus_succ_l; now rewrite H.
+do 2 rewrite add_succ_l; now rewrite H.
 Qed.
 
 Add Morphism NZpred with signature Zeq ==> Zeq as NZpred_wd.
 Proof.
 unfold NZpred, Zeq; intros n m H; simpl.
-do 2 rewrite plus_succ_r; now rewrite H.
+do 2 rewrite add_succ_r; now rewrite H.
 Qed.
 
-Add Morphism NZplus with signature Zeq ==> Zeq ==> Zeq as NZplus_wd.
+Add Morphism NZadd with signature Zeq ==> Zeq ==> Zeq as NZadd_wd.
 Proof.
-unfold Zeq, NZplus; intros n1 m1 H1 n2 m2 H2; simpl.
+unfold Zeq, NZadd; intros n1 m1 H1 n2 m2 H2; simpl.
 assert (H3 : (fst n1 + snd m1) + (fst n2 + snd m2) == (fst m1 + snd n1) + (fst m2 + snd n2))
-by now apply plus_wd.
+by now apply add_wd.
 stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring.
 now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring.
 Qed.
@@ -167,28 +167,28 @@ Proof.
 unfold Zeq, NZminus; intros n1 m1 H1 n2 m2 H2; simpl.
 symmetry in H2.
 assert (H3 : (fst n1 + snd m1) + (fst m2 + snd n2) == (fst m1 + snd n1) + (fst n2 + snd m2))
-by now apply plus_wd.
+by now apply add_wd.
 stepl (fst n1 + snd m1 + (fst m2 + snd n2)) by ring.
 now stepr (fst m1 + snd n1 + (fst n2 + snd m2)) by ring.
 Qed.
 
-Add Morphism NZtimes with signature Zeq ==> Zeq ==> Zeq as NZtimes_wd.
+Add Morphism NZmul with signature Zeq ==> Zeq ==> Zeq as NZmul_wd.
 Proof.
-unfold NZtimes, Zeq; intros n1 m1 H1 n2 m2 H2; simpl.
+unfold NZmul, Zeq; intros n1 m1 H1 n2 m2 H2; simpl.
 stepl (fst n1 * fst n2 + (snd n1 * snd n2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
 stepr (fst n1 * snd n2 + (fst m1 * fst m2 + snd m1 * snd m2 + snd n1 * fst n2)) by ring.
-apply plus_times_repl_pair with (n := fst m2) (m := snd m2); [| now idtac].
+apply add_mul_repl_pair with (n := fst m2) (m := snd m2); [| now idtac].
 stepl (snd n1 * snd n2 + (fst n1 * fst m2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
 stepr (snd n1 * fst n2 + (fst n1 * snd m2 + fst m1 * fst m2 + snd m1 * snd m2)) by ring.
-apply plus_times_repl_pair with (n := snd m2) (m := fst m2);
+apply add_mul_repl_pair with (n := snd m2) (m := fst m2);
 [| (stepl (fst n2 + snd m2) by ring); now stepr (fst m2 + snd n2) by ring].
 stepl (snd m2 * snd n1 + (fst n1 * fst m2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
 stepr (snd m2 * fst n1 + (snd n1 * fst m2 + fst m1 * fst m2 + snd m1 * snd m2)) by ring.
-apply plus_times_repl_pair with (n := snd m1) (m := fst m1);
+apply add_mul_repl_pair with (n := snd m1) (m := fst m1);
 [ | (stepl (fst n1 + snd m1) by ring); now stepr (fst m1 + snd n1) by ring].
 stepl (fst m2 * fst n1 + (snd m2 * snd m1 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
 stepr (fst m2 * snd n1 + (snd m2 * fst m1 + fst m1 * fst m2 + snd m1 * snd m2)) by ring.
-apply plus_times_repl_pair with (n := fst m1) (m := snd m1); [| now idtac].
+apply add_mul_repl_pair with (n := fst m1) (m := snd m1); [| now idtac].
 ring.
 Qed.
 
@@ -209,12 +209,12 @@ intros A0 AS n; unfold NZ0, Zsucc, predicate_wd, fun_wd, Zeq in *.
 destruct n as [n m].
 cut (forall p : N, A (p, 0)); [intro H1 |].
 cut (forall p : N, A (0, p)); [intro H2 |].
-destruct (plus_dichotomy n m) as [[p H] | [p H]].
-rewrite (A_wd (n, m) (0, p)) by (rewrite plus_0_l; now rewrite plus_comm).
+destruct (add_dichotomy n m) as [[p H] | [p H]].
+rewrite (A_wd (n, m) (0, p)) by (rewrite add_0_l; now rewrite add_comm).
 apply H2.
-rewrite (A_wd (n, m) (p, 0)) by now rewrite plus_0_r. apply H1.
+rewrite (A_wd (n, m) (p, 0)) by now rewrite add_0_r. apply H1.
 induct p. assumption. intros p IH.
-apply -> (A_wd (0, p) (1, S p)) in IH; [| now rewrite plus_0_l, plus_1_l].
+apply -> (A_wd (0, p) (1, S p)) in IH; [| now rewrite add_0_l, add_1_l].
 now apply <- AS.
 induct p. assumption. intros p IH.
 replace 0 with (snd (p, 0)); [| reflexivity].
@@ -230,39 +230,39 @@ Open Local Scope IntScope.
 Theorem NZpred_succ : forall n : Z, Zpred (Zsucc n) == n.
 Proof.
 unfold NZpred, NZsucc, Zeq; intro n; simpl.
-rewrite plus_succ_l; now rewrite plus_succ_r.
+rewrite add_succ_l; now rewrite add_succ_r.
 Qed.
 
-Theorem NZplus_0_l : forall n : Z, 0 + n == n.
+Theorem NZadd_0_l : forall n : Z, 0 + n == n.
 Proof.
-intro n; unfold NZplus, Zeq; simpl. now do 2 rewrite plus_0_l.
+intro n; unfold NZadd, Zeq; simpl. now do 2 rewrite add_0_l.
 Qed.
 
-Theorem NZplus_succ_l : forall n m : Z, (Zsucc n) + m == Zsucc (n + m).
+Theorem NZadd_succ_l : forall n m : Z, (Zsucc n) + m == Zsucc (n + m).
 Proof.
-intros n m; unfold NZplus, Zeq; simpl. now do 2 rewrite plus_succ_l.
+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.
 Proof.
-intro n; unfold NZminus, Zeq; simpl. now do 2 rewrite plus_0_r.
+intro n; unfold NZminus, Zeq; simpl. now do 2 rewrite add_0_r.
 Qed.
 
 Theorem NZminus_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m).
 Proof.
-intros n m; unfold NZminus, Zeq; simpl. symmetry; now rewrite plus_succ_r.
+intros n m; unfold NZminus, Zeq; simpl. symmetry; now rewrite add_succ_r.
 Qed.
 
-Theorem NZtimes_0_l : forall n : Z, 0 * n == 0.
+Theorem NZmul_0_l : forall n : Z, 0 * n == 0.
 Proof.
-intro n; unfold NZtimes, Zeq; simpl.
-repeat rewrite times_0_l. now rewrite plus_assoc.
+intro n; unfold NZmul, Zeq; simpl.
+repeat rewrite mul_0_l. now rewrite add_assoc.
 Qed.
 
-Theorem NZtimes_succ_l : forall n m : Z, (Zsucc n) * m == n * m + m.
+Theorem NZmul_succ_l : forall n m : Z, (Zsucc n) * m == n * m + m.
 Proof.
-intros n m; unfold NZtimes, NZsucc, Zeq; simpl.
-do 2 rewrite times_succ_l. ring.
+intros n m; unfold NZmul, NZsucc, Zeq; simpl.
+do 2 rewrite mul_succ_l. ring.
 Qed.
 
 End NZAxiomsMod.
@@ -275,20 +275,20 @@ Definition NZmax := Zmax.
 Add Morphism NZlt with signature Zeq ==> Zeq ==> iff as NZlt_wd.
 Proof.
 unfold NZlt, Zlt, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H.
-stepr (snd m1 + fst m2) by apply plus_comm.
-apply (plus_lt_repl_pair (fst n1) (snd n1)); [| assumption].
-stepl (snd m2 + fst n1) by apply plus_comm.
-stepr (fst m2 + snd n1) by apply plus_comm.
-apply (plus_lt_repl_pair (snd n2) (fst n2)).
-now stepl (fst n1 + snd n2) by apply plus_comm.
-stepl (fst m2 + snd n2) by apply plus_comm. now stepr (fst n2 + snd m2) by apply plus_comm.
-stepr (snd n1 + fst n2) by apply plus_comm.
-apply (plus_lt_repl_pair (fst m1) (snd m1)); [| now symmetry].
-stepl (snd n2 + fst m1) by apply plus_comm.
-stepr (fst n2 + snd m1) by apply plus_comm.
-apply (plus_lt_repl_pair (snd m2) (fst m2)).
-now stepl (fst m1 + snd m2) by apply plus_comm.
-stepl (fst n2 + snd m2) by apply plus_comm. now stepr (fst m2 + snd n2) by apply plus_comm.
+stepr (snd m1 + fst m2) by apply add_comm.
+apply (add_lt_repl_pair (fst n1) (snd n1)); [| assumption].
+stepl (snd m2 + fst n1) by apply add_comm.
+stepr (fst m2 + snd n1) by apply add_comm.
+apply (add_lt_repl_pair (snd n2) (fst n2)).
+now stepl (fst n1 + snd n2) by apply add_comm.
+stepl (fst m2 + snd n2) by apply add_comm. now stepr (fst n2 + snd m2) by apply add_comm.
+stepr (snd n1 + fst n2) by apply add_comm.
+apply (add_lt_repl_pair (fst m1) (snd m1)); [| now symmetry].
+stepl (snd n2 + fst m1) by apply add_comm.
+stepr (fst n2 + snd m1) by apply add_comm.
+apply (add_lt_repl_pair (snd m2) (fst m2)).
+now stepl (fst m1 + snd m2) by apply add_comm.
+stepl (fst n2 + snd m2) by apply add_comm. now stepr (fst m2 + snd n2) by apply add_comm.
 Qed.
 
 Add Morphism NZle with signature Zeq ==> Zeq ==> iff as NZle_wd.
@@ -345,7 +345,7 @@ Qed.
 
 Theorem NZlt_succ_r : forall n m : Z, n < (Zsucc m) <-> n <= m.
 Proof.
-intros n m; unfold Zlt, Zle, Zeq; simpl. rewrite plus_succ_l; apply lt_succ_r.
+intros n m; unfold Zlt, Zle, Zeq; simpl. rewrite add_succ_l; apply lt_succ_r.
 Qed.
 
 Theorem NZmin_l : forall n m : Z, n <= m -> Zmin n m == n.
@@ -381,8 +381,8 @@ Notation "- x" := (Zopp x) : IntScope.
 Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd.
 Proof.
 unfold Zeq; intros n m H; simpl. symmetry.
-stepl (fst n + snd m) by apply plus_comm.
-now stepr (fst m + snd n) by apply plus_comm.
+stepl (fst n + snd m) by apply add_comm.
+now stepr (fst m + snd n) by apply add_comm.
 Qed.
 
 Open Local Scope IntScope.
@@ -390,12 +390,12 @@ Open Local Scope IntScope.
 Theorem Zsucc_pred : forall n : Z, Zsucc (Zpred n) == n.
 Proof.
 intro n; unfold Zsucc, Zpred, Zeq; simpl.
-rewrite plus_succ_l; now rewrite plus_succ_r.
+rewrite add_succ_l; now rewrite add_succ_r.
 Qed.
 
 Theorem Zopp_0 : - 0 == 0.
 Proof.
-unfold Zopp, Zeq; simpl. now rewrite plus_0_l.
+unfold Zopp, Zeq; simpl. now rewrite add_0_l.
 Qed.
 
 Theorem Zopp_succ : forall n, - (Zsucc n) == Zpred (- n).
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 3d9d3d190..bb56e6997 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -41,9 +41,9 @@ Definition NZeq := Z.eq.
 Definition NZ0 := Z.zero.
 Definition NZsucc := Z.succ.
 Definition NZpred := Z.pred.
-Definition NZplus := Z.add.
+Definition NZadd := Z.add.
 Definition NZminus := Z.sub.
-Definition NZtimes := Z.mul.
+Definition NZmul := Z.mul.
 
 Theorem NZeq_equiv : equiv Z.t Z.eq.
 Proof.
@@ -66,7 +66,7 @@ Proof.
 intros; zsimpl; f_equal; assumption.
 Qed.
 
-Add Morphism NZplus with signature Z.eq ==> Z.eq ==> Z.eq as NZplus_wd.
+Add Morphism NZadd with signature Z.eq ==> Z.eq ==> Z.eq as NZadd_wd.
 Proof.
 intros; zsimpl; f_equal; assumption.
 Qed.
@@ -76,7 +76,7 @@ Proof.
 intros; zsimpl; f_equal; assumption.
 Qed.
 
-Add Morphism NZtimes with signature Z.eq ==> Z.eq ==> Z.eq as NZtimes_wd.
+Add Morphism NZmul with signature Z.eq ==> Z.eq ==> Z.eq as NZmul_wd.
 Proof.
 intros; zsimpl; f_equal; assumption.
 Qed.
@@ -144,12 +144,12 @@ Qed.
 
 End Induction.
 
-Theorem NZplus_0_l : forall n, 0 + n == n.
+Theorem NZadd_0_l : forall n, 0 + n == n.
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem NZplus_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m).
+Theorem NZadd_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m).
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.
@@ -164,12 +164,12 @@ Proof.
 intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem NZtimes_0_l : forall n, 0 * n == 0.
+Theorem NZmul_0_l : forall n, 0 * n == 0.
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem NZtimes_succ_l : forall n m, (Z.succ n) * m == n * m + m.
+Theorem NZmul_succ_l : forall n m, (Z.succ n) * m == n * m + m.
 Proof.
 intros; zsimpl; ring.
 Qed.