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

6 files changed, 375 insertions, 375 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 678781b23c..19fb40dfee 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 c57f9ede0c..0b8538873e 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 2520d62e19..d72d00379c 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 3e6421819b..85f6714987 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 2d7ff30f77..ccf324a062 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 6b6f34d75e..d3f5a03963 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.