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

28 files changed, 1004 insertions, 1004 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 2d23a12dd..113945e0d 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -39,9 +39,9 @@ Definition NZeq (n m : NZ) := [| n |] = [| m |].
 Definition NZ0 := w_op.(znz_0).
 Definition NZsucc := w_op.(znz_succ).
 Definition NZpred := w_op.(znz_pred).
-Definition NZplus := w_op.(znz_add).
+Definition NZadd := w_op.(znz_add).
 Definition NZminus := w_op.(znz_sub).
-Definition NZtimes := w_op.(znz_mul).
+Definition NZmul := w_op.(znz_mul).
 
 Theorem NZeq_equiv : equiv NZ NZeq.
 Proof.
@@ -65,7 +65,7 @@ Proof.
 unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_pred). now rewrite H.
 Qed.
 
-Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd.
+Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.
 Proof.
 unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add).
 now rewrite H1, H2.
@@ -77,7 +77,7 @@ unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub).
 now rewrite H1, H2.
 Qed.
 
-Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd.
+Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.
 Proof.
 unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_mul).
 now rewrite H1, H2.
@@ -92,9 +92,9 @@ Notation "0" := NZ0 : IntScope.
 Notation "'S'" := NZsucc : IntScope.
 Notation "'P'" := NZpred : IntScope.
 (*Notation "1" := (S 0) : IntScope.*)
-Notation "x + y" := (NZplus x y) : IntScope.
+Notation "x + y" := (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.
 
 Theorem gt_wB_1 : 1 < wB.
 Proof.
@@ -189,15 +189,15 @@ Qed.
 
 End Induction.
 
-Theorem NZplus_0_l : forall n : NZ, 0 + n == n.
+Theorem NZadd_0_l : forall n : NZ, 0 + n == n.
 Proof.
-intro n; unfold NZplus, NZ0, NZeq. rewrite w_spec.(spec_add). rewrite w_spec.(spec_0).
+intro n; unfold NZadd, NZ0, NZeq. rewrite w_spec.(spec_add). rewrite w_spec.(spec_0).
 rewrite Zplus_0_l. rewrite Zmod_small; [reflexivity | apply w_spec.(spec_to_Z)].
 Qed.
 
-Theorem NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m).
+Theorem NZadd_succ_l : forall n m : NZ, (S n) + m == S (n + m).
 Proof.
-intros n m; unfold NZplus, NZsucc, NZeq. rewrite w_spec.(spec_add).
+intros n m; unfold NZadd, NZsucc, NZeq. rewrite w_spec.(spec_add).
 do 2 rewrite w_spec.(spec_succ). rewrite w_spec.(spec_add).
 rewrite NZsucc_mod_wB. repeat rewrite Zplus_mod_idemp_l; try apply gt_wB_0.
 rewrite <- (Zplus_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l.
@@ -219,15 +219,15 @@ rewrite Zminus_mod_idemp_l.
 now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z by auto with zarith.
 Qed.
 
-Theorem NZtimes_0_l : forall n : NZ, 0 * n == 0.
+Theorem NZmul_0_l : forall n : NZ, 0 * n == 0.
 Proof.
-intro n; unfold NZtimes, NZ0, NZ, NZeq. rewrite w_spec.(spec_mul).
+intro n; unfold NZmul, NZ0, NZ, NZeq. rewrite w_spec.(spec_mul).
 rewrite w_spec.(spec_0). now rewrite Zmult_0_l.
 Qed.
 
-Theorem NZtimes_succ_l : forall n m : NZ, (S n) * m == n * m + m.
+Theorem NZmul_succ_l : forall n m : NZ, (S n) * m == n * m + m.
 Proof.
-intros n m; unfold NZtimes, NZsucc, NZplus, NZeq. rewrite w_spec.(spec_mul).
+intros n m; unfold NZmul, NZsucc, NZadd, NZeq. rewrite w_spec.(spec_mul).
 rewrite w_spec.(spec_add), w_spec.(spec_mul), w_spec.(spec_succ).
 rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l.
 now rewrite Zmult_plus_distr_l, Zmult_1_l.
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.
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index ef1906995..516cf5b42 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -19,9 +19,9 @@ Parameter Inline NZeq : NZ -> NZ -> Prop.
 Parameter Inline NZ0 : NZ.
 Parameter Inline NZsucc : NZ -> NZ.
 Parameter Inline NZpred : NZ -> NZ.
-Parameter Inline NZplus : NZ -> NZ -> NZ.
+Parameter Inline NZadd : NZ -> NZ -> NZ.
 Parameter Inline NZminus : NZ -> NZ -> NZ.
-Parameter Inline NZtimes : NZ -> NZ -> NZ.
+Parameter Inline NZmul : NZ -> NZ -> NZ.
 
 (* Unary minus (opp) is not defined on natural numbers, so we have it for
 integers only *)
@@ -35,9 +35,9 @@ as NZeq_rel.
 
 Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
 Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
-Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd.
+Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.
 Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd.
-Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd.
+Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.
 
 Delimit Scope NatIntScope with NatInt.
 Open Local Scope NatIntScope.
@@ -47,9 +47,9 @@ Notation "0" := NZ0 : NatIntScope.
 Notation S := NZsucc.
 Notation P := NZpred.
 Notation "1" := (S 0) : NatIntScope.
-Notation "x + y" := (NZplus x y) : NatIntScope.
+Notation "x + y" := (NZadd x y) : NatIntScope.
 Notation "x - y" := (NZminus x y) : NatIntScope.
-Notation "x * y" := (NZtimes x y) : NatIntScope.
+Notation "x * y" := (NZmul x y) : NatIntScope.
 
 Axiom NZpred_succ : forall n : NZ, P (S n) == n.
 
@@ -57,14 +57,14 @@ Axiom NZinduction :
   forall A : NZ -> Prop, predicate_wd NZeq A ->
     A 0 -> (forall n : NZ, A n <-> A (S n)) -> forall n : NZ, A n.
 
-Axiom NZplus_0_l : forall n : NZ, 0 + n == n.
-Axiom NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m).
+Axiom NZadd_0_l : forall n : NZ, 0 + n == n.
+Axiom NZadd_succ_l : forall n m : NZ, (S n) + m == S (n + m).
 
 Axiom NZminus_0_r : forall n : NZ, n - 0 == n.
 Axiom NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m).
 
-Axiom NZtimes_0_l : forall n : NZ, 0 * n == 0.
-Axiom NZtimes_succ_l : forall n m : NZ, S n * m == n * m + m.
+Axiom NZmul_0_l : forall n : NZ, 0 * n == 0.
+Axiom NZmul_succ_l : forall n m : NZ, S n * m == n * m + m.
 
 End NZAxiomsSig.
 
diff --git a/theories/Numbers/NatInt/NZPlus.v b/theories/Numbers/NatInt/NZPlus.v
index 673b819ba..6fb72ed4a 100644
--- a/theories/Numbers/NatInt/NZPlus.v
+++ b/theories/Numbers/NatInt/NZPlus.v
@@ -17,69 +17,69 @@ Module NZPlusPropFunct (Import NZAxiomsMod : NZAxiomsSig).
 Module Export NZBasePropMod := NZBasePropFunct NZAxiomsMod.
 Open Local Scope NatIntScope.
 
-Theorem NZplus_0_r : forall n : NZ, n + 0 == n.
+Theorem NZadd_0_r : forall n : NZ, n + 0 == n.
 Proof.
-NZinduct n. now rewrite NZplus_0_l.
-intro. rewrite NZplus_succ_l. now rewrite NZsucc_inj_wd.
+NZinduct n. now rewrite NZadd_0_l.
+intro. rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd.
 Qed.
 
-Theorem NZplus_succ_r : forall n m : NZ, n + S m == S (n + m).
+Theorem NZadd_succ_r : forall n m : NZ, n + S m == S (n + m).
 Proof.
 intros n m; NZinduct n.
-now do 2 rewrite NZplus_0_l.
-intro. repeat rewrite NZplus_succ_l. now rewrite NZsucc_inj_wd.
+now do 2 rewrite NZadd_0_l.
+intro. repeat rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd.
 Qed.
 
-Theorem NZplus_comm : forall n m : NZ, n + m == m + n.
+Theorem NZadd_comm : forall n m : NZ, n + m == m + n.
 Proof.
 intros n m; NZinduct n.
-rewrite NZplus_0_l; now rewrite NZplus_0_r.
-intros n. rewrite NZplus_succ_l; rewrite NZplus_succ_r. now rewrite NZsucc_inj_wd.
+rewrite NZadd_0_l; now rewrite NZadd_0_r.
+intros n. rewrite NZadd_succ_l; rewrite NZadd_succ_r. now rewrite NZsucc_inj_wd.
 Qed.
 
-Theorem NZplus_1_l : forall n : NZ, 1 + n == S n.
+Theorem NZadd_1_l : forall n : NZ, 1 + n == S n.
 Proof.
-intro n; rewrite NZplus_succ_l; now rewrite NZplus_0_l.
+intro n; rewrite NZadd_succ_l; now rewrite NZadd_0_l.
 Qed.
 
-Theorem NZplus_1_r : forall n : NZ, n + 1 == S n.
+Theorem NZadd_1_r : forall n : NZ, n + 1 == S n.
 Proof.
-intro n; rewrite NZplus_comm; apply NZplus_1_l.
+intro n; rewrite NZadd_comm; apply NZadd_1_l.
 Qed.
 
-Theorem NZplus_assoc : forall n m p : NZ, n + (m + p) == (n + m) + p.
+Theorem NZadd_assoc : forall n m p : NZ, n + (m + p) == (n + m) + p.
 Proof.
 intros n m p; NZinduct n.
-now do 2 rewrite NZplus_0_l.
-intro. do 3 rewrite NZplus_succ_l. now rewrite NZsucc_inj_wd.
+now do 2 rewrite NZadd_0_l.
+intro. do 3 rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd.
 Qed.
 
-Theorem NZplus_shuffle1 : forall n m p q : NZ, (n + m) + (p + q) == (n + p) + (m + q).
+Theorem NZadd_shuffle1 : forall n m p q : NZ, (n + m) + (p + q) == (n + p) + (m + q).
 Proof.
 intros n m p q.
-rewrite <- (NZplus_assoc n m (p + q)). rewrite (NZplus_comm m (p + q)).
-rewrite <- (NZplus_assoc p q m). rewrite (NZplus_assoc n p (q + m)).
-now rewrite (NZplus_comm q m).
+rewrite <- (NZadd_assoc n m (p + q)). rewrite (NZadd_comm m (p + q)).
+rewrite <- (NZadd_assoc p q m). rewrite (NZadd_assoc n p (q + m)).
+now rewrite (NZadd_comm q m).
 Qed.
 
-Theorem NZplus_shuffle2 : forall n m p q : NZ, (n + m) + (p + q) == (n + q) + (m + p).
+Theorem NZadd_shuffle2 : forall n m p q : NZ, (n + m) + (p + q) == (n + q) + (m + p).
 Proof.
 intros n m p q.
-rewrite <- (NZplus_assoc n m (p + q)). rewrite (NZplus_assoc m p q).
-rewrite (NZplus_comm (m + p) q). now rewrite <- (NZplus_assoc n q (m + p)).
+rewrite <- (NZadd_assoc n m (p + q)). rewrite (NZadd_assoc m p q).
+rewrite (NZadd_comm (m + p) q). now rewrite <- (NZadd_assoc n q (m + p)).
 Qed.
 
-Theorem NZplus_cancel_l : forall n m p : NZ, p + n == p + m <-> n == m.
+Theorem NZadd_cancel_l : forall n m p : NZ, p + n == p + m <-> n == m.
 Proof.
 intros n m p; NZinduct p.
-now do 2 rewrite NZplus_0_l.
-intro p. do 2 rewrite NZplus_succ_l. now rewrite NZsucc_inj_wd.
+now do 2 rewrite NZadd_0_l.
+intro p. do 2 rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd.
 Qed.
 
-Theorem NZplus_cancel_r : forall n m p : NZ, n + p == m + p <-> n == m.
+Theorem NZadd_cancel_r : forall n m p : NZ, n + p == m + p <-> n == m.
 Proof.
-intros n m p. rewrite (NZplus_comm n p); rewrite (NZplus_comm m p).
-apply NZplus_cancel_l.
+intros n m p. rewrite (NZadd_comm n p); rewrite (NZadd_comm m p).
+apply NZadd_cancel_l.
 Qed.
 
 Theorem NZminus_1_r : forall n : NZ, n - 1 == P n.
diff --git a/theories/Numbers/NatInt/NZPlusOrder.v b/theories/Numbers/NatInt/NZPlusOrder.v
index 45148bc20..00d178c0d 100644
--- a/theories/Numbers/NatInt/NZPlusOrder.v
+++ b/theories/Numbers/NatInt/NZPlusOrder.v
@@ -17,149 +17,149 @@ Module NZPlusOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig).
 Module Export NZOrderPropMod := NZOrderPropFunct NZOrdAxiomsMod.
 Open Local Scope NatIntScope.
 
-Theorem NZplus_lt_mono_l : forall n m p : NZ, n < m <-> p + n < p + m.
+Theorem NZadd_lt_mono_l : forall n m p : NZ, n < m <-> p + n < p + m.
 Proof.
 intros n m p; NZinduct p.
-now do 2 rewrite NZplus_0_l.
-intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_lt_mono.
+now do 2 rewrite NZadd_0_l.
+intro p. do 2 rewrite NZadd_succ_l. now rewrite <- NZsucc_lt_mono.
 Qed.
 
-Theorem NZplus_lt_mono_r : forall n m p : NZ, n < m <-> n + p < m + p.
+Theorem NZadd_lt_mono_r : forall n m p : NZ, n < m <-> n + p < m + p.
 Proof.
 intros n m p.
-rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_lt_mono_l.
+rewrite (NZadd_comm n p); rewrite (NZadd_comm m p); apply NZadd_lt_mono_l.
 Qed.
 
-Theorem NZplus_lt_mono : forall n m p q : NZ, n < m -> p < q -> n + p < m + q.
+Theorem NZadd_lt_mono : forall n m p q : NZ, n < m -> p < q -> n + p < m + q.
 Proof.
 intros n m p q H1 H2.
 apply NZlt_trans with (m + p);
-[now apply -> NZplus_lt_mono_r | now apply -> NZplus_lt_mono_l].
+[now apply -> NZadd_lt_mono_r | now apply -> NZadd_lt_mono_l].
 Qed.
 
-Theorem NZplus_le_mono_l : forall n m p : NZ, n <= m <-> p + n <= p + m.
+Theorem NZadd_le_mono_l : forall n m p : NZ, n <= m <-> p + n <= p + m.
 Proof.
 intros n m p; NZinduct p.
-now do 2 rewrite NZplus_0_l.
-intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_le_mono.
+now do 2 rewrite NZadd_0_l.
+intro p. do 2 rewrite NZadd_succ_l. now rewrite <- NZsucc_le_mono.
 Qed.
 
-Theorem NZplus_le_mono_r : forall n m p : NZ, n <= m <-> n + p <= m + p.
+Theorem NZadd_le_mono_r : forall n m p : NZ, n <= m <-> n + p <= m + p.
 Proof.
 intros n m p.
-rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_le_mono_l.
+rewrite (NZadd_comm n p); rewrite (NZadd_comm m p); apply NZadd_le_mono_l.
 Qed.
 
-Theorem NZplus_le_mono : forall n m p q : NZ, n <= m -> p <= q -> n + p <= m + q.
+Theorem NZadd_le_mono : forall n m p q : NZ, n <= m -> p <= q -> n + p <= m + q.
 Proof.
 intros n m p q H1 H2.
 apply NZle_trans with (m + p);
-[now apply -> NZplus_le_mono_r | now apply -> NZplus_le_mono_l].
+[now apply -> NZadd_le_mono_r | now apply -> NZadd_le_mono_l].
 Qed.
 
-Theorem NZplus_lt_le_mono : forall n m p q : NZ, n < m -> p <= q -> n + p < m + q.
+Theorem NZadd_lt_le_mono : forall n m p q : NZ, n < m -> p <= q -> n + p < m + q.
 Proof.
 intros n m p q H1 H2.
 apply NZlt_le_trans with (m + p);
-[now apply -> NZplus_lt_mono_r | now apply -> NZplus_le_mono_l].
+[now apply -> NZadd_lt_mono_r | now apply -> NZadd_le_mono_l].
 Qed.
 
-Theorem NZplus_le_lt_mono : forall n m p q : NZ, n <= m -> p < q -> n + p < m + q.
+Theorem NZadd_le_lt_mono : forall n m p q : NZ, n <= m -> p < q -> n + p < m + q.
 Proof.
 intros n m p q H1 H2.
 apply NZle_lt_trans with (m + p);
-[now apply -> NZplus_le_mono_r | now apply -> NZplus_lt_mono_l].
+[now apply -> NZadd_le_mono_r | now apply -> NZadd_lt_mono_l].
 Qed.
 
-Theorem NZplus_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n + m.
+Theorem NZadd_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n + m.
 Proof.
-intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_lt_mono.
+intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_lt_mono.
 Qed.
 
-Theorem NZplus_pos_nonneg : forall n m : NZ, 0 < n -> 0 <= m -> 0 < n + m.
+Theorem NZadd_pos_nonneg : forall n m : NZ, 0 < n -> 0 <= m -> 0 < n + m.
 Proof.
-intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_lt_le_mono.
+intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_lt_le_mono.
 Qed.
 
-Theorem NZplus_nonneg_pos : forall n m : NZ, 0 <= n -> 0 < m -> 0 < n + m.
+Theorem NZadd_nonneg_pos : forall n m : NZ, 0 <= n -> 0 < m -> 0 < n + m.
 Proof.
-intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_le_lt_mono.
+intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_le_lt_mono.
 Qed.
 
-Theorem NZplus_nonneg_nonneg : forall n m : NZ, 0 <= n -> 0 <= m -> 0 <= n + m.
+Theorem NZadd_nonneg_nonneg : forall n m : NZ, 0 <= n -> 0 <= m -> 0 <= n + m.
 Proof.
-intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_le_mono.
+intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_le_mono.
 Qed.
 
-Theorem NZlt_plus_pos_l : forall n m : NZ, 0 < n -> m < n + m.
+Theorem NZlt_add_pos_l : forall n m : NZ, 0 < n -> m < n + m.
 Proof.
-intros n m H. apply -> (NZplus_lt_mono_r 0 n m) in H.
-now rewrite NZplus_0_l in H.
+intros n m H. apply -> (NZadd_lt_mono_r 0 n m) in H.
+now rewrite NZadd_0_l in H.
 Qed.
 
-Theorem NZlt_plus_pos_r : forall n m : NZ, 0 < n -> m < m + n.
+Theorem NZlt_add_pos_r : forall n m : NZ, 0 < n -> m < m + n.
 Proof.
-intros; rewrite NZplus_comm; now apply NZlt_plus_pos_l.
+intros; rewrite NZadd_comm; now apply NZlt_add_pos_l.
 Qed.
 
-Theorem NZle_lt_plus_lt : forall n m p q : NZ, n <= m -> p + m < q + n -> p < q.
+Theorem NZle_lt_add_lt : forall n m p q : NZ, n <= m -> p + m < q + n -> p < q.
 Proof.
 intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption].
-pose proof (NZplus_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H2.
+pose proof (NZadd_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H2.
 false_hyp H3 H2.
 Qed.
 
-Theorem NZlt_le_plus_lt : forall n m p q : NZ, n < m -> p + m <= q + n -> p < q.
+Theorem NZlt_le_add_lt : forall n m p q : NZ, n < m -> p + m <= q + n -> p < q.
 Proof.
 intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption].
-pose proof (NZplus_le_lt_mono q p n m H H1) as H3. apply <- NZnle_gt in H3.
+pose proof (NZadd_le_lt_mono q p n m H H1) as H3. apply <- NZnle_gt in H3.
 false_hyp H2 H3.
 Qed.
 
-Theorem NZle_le_plus_le : forall n m p q : NZ, n <= m -> p + m <= q + n -> p <= q.
+Theorem NZle_le_add_le : forall n m p q : NZ, n <= m -> p + m <= q + n -> p <= q.
 Proof.
 intros n m p q H1 H2. destruct (NZle_gt_cases p q); [assumption |].
-pose proof (NZplus_lt_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H3.
+pose proof (NZadd_lt_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H3.
 false_hyp H2 H3.
 Qed.
 
-Theorem NZplus_lt_cases : forall n m p q : NZ, n + m < p + q -> n < p \/ m < q.
+Theorem NZadd_lt_cases : forall n m p q : NZ, n + m < p + q -> n < p \/ m < q.
 Proof.
 intros n m p q H;
 destruct (NZle_gt_cases p n) as [H1 | H1].
 destruct (NZle_gt_cases q m) as [H2 | H2].
-pose proof (NZplus_le_mono p n q m H1 H2) as H3. apply -> NZle_ngt in H3.
+pose proof (NZadd_le_mono p n q m H1 H2) as H3. apply -> NZle_ngt in H3.
 false_hyp H H3.
 now right. now left.
 Qed.
 
-Theorem NZplus_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q.
+Theorem NZadd_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q.
 Proof.
 intros n m p q H.
 destruct (NZle_gt_cases n p) as [H1 | H1]. now left.
 destruct (NZle_gt_cases m q) as [H2 | H2]. now right.
-assert (H3 : p + q < n + m) by now apply NZplus_lt_mono.
+assert (H3 : p + q < n + m) by now apply NZadd_lt_mono.
 apply -> NZle_ngt in H. false_hyp H3 H.
 Qed.
 
-Theorem NZplus_neg_cases : forall n m : NZ, n + m < 0 -> n < 0 \/ m < 0.
+Theorem NZadd_neg_cases : forall n m : NZ, n + m < 0 -> n < 0 \/ m < 0.
 Proof.
-intros n m H; apply NZplus_lt_cases; now rewrite NZplus_0_l.
+intros n m H; apply NZadd_lt_cases; now rewrite NZadd_0_l.
 Qed.
 
-Theorem NZplus_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m.
+Theorem NZadd_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m.
 Proof.
-intros n m H; apply NZplus_lt_cases; now rewrite NZplus_0_l.
+intros n m H; apply NZadd_lt_cases; now rewrite NZadd_0_l.
 Qed.
 
-Theorem NZplus_nonpos_cases : forall n m : NZ, n + m <= 0 -> n <= 0 \/ m <= 0.
+Theorem NZadd_nonpos_cases : forall n m : NZ, n + m <= 0 -> n <= 0 \/ m <= 0.
 Proof.
-intros n m H; apply NZplus_le_cases; now rewrite NZplus_0_l.
+intros n m H; apply NZadd_le_cases; now rewrite NZadd_0_l.
 Qed.
 
-Theorem NZplus_nonneg_cases : forall n m : NZ, 0 <= n + m -> 0 <= n \/ 0 <= m.
+Theorem NZadd_nonneg_cases : forall n m : NZ, 0 <= n + m -> 0 <= n \/ 0 <= m.
 Proof.
-intros n m H; apply NZplus_le_cases; now rewrite NZplus_0_l.
+intros n m H; apply NZadd_le_cases; now rewrite NZadd_0_l.
 Qed.
 
 End NZPlusOrderPropFunct.
diff --git a/theories/Numbers/NatInt/NZTimes.v b/theories/Numbers/NatInt/NZTimes.v
index 7503ddce2..9f93e0a1b 100644
--- a/theories/Numbers/NatInt/NZTimes.v
+++ b/theories/Numbers/NatInt/NZTimes.v
@@ -17,63 +17,63 @@ Module NZTimesPropFunct (Import NZAxiomsMod : NZAxiomsSig).
 Module Export NZPlusPropMod := NZPlusPropFunct NZAxiomsMod.
 Open Local Scope NatIntScope.
 
-Theorem NZtimes_0_r : forall n : NZ, n * 0 == 0.
+Theorem NZmul_0_r : forall n : NZ, n * 0 == 0.
 Proof.
 NZinduct n.
-now rewrite NZtimes_0_l.
-intro. rewrite NZtimes_succ_l. now rewrite NZplus_0_r.
+now rewrite NZmul_0_l.
+intro. rewrite NZmul_succ_l. now rewrite NZadd_0_r.
 Qed.
 
-Theorem NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n.
+Theorem NZmul_succ_r : forall n m : NZ, n * (S m) == n * m + n.
 Proof.
 intros n m; NZinduct n.
-do 2 rewrite NZtimes_0_l; now rewrite NZplus_0_l.
-intro n. do 2 rewrite NZtimes_succ_l. do 2 rewrite NZplus_succ_r.
-rewrite NZsucc_inj_wd. rewrite <- (NZplus_assoc (n * m) m n).
-rewrite (NZplus_comm m n). rewrite NZplus_assoc.
-now rewrite NZplus_cancel_r.
+do 2 rewrite NZmul_0_l; now rewrite NZadd_0_l.
+intro n. do 2 rewrite NZmul_succ_l. do 2 rewrite NZadd_succ_r.
+rewrite NZsucc_inj_wd. rewrite <- (NZadd_assoc (n * m) m n).
+rewrite (NZadd_comm m n). rewrite NZadd_assoc.
+now rewrite NZadd_cancel_r.
 Qed.
 
-Theorem NZtimes_comm : forall n m : NZ, n * m == m * n.
+Theorem NZmul_comm : forall n m : NZ, n * m == m * n.
 Proof.
 intros n m; NZinduct n.
-rewrite NZtimes_0_l; now rewrite NZtimes_0_r.
-intro. rewrite NZtimes_succ_l; rewrite NZtimes_succ_r. now rewrite NZplus_cancel_r.
+rewrite NZmul_0_l; now rewrite NZmul_0_r.
+intro. rewrite NZmul_succ_l; rewrite NZmul_succ_r. now rewrite NZadd_cancel_r.
 Qed.
 
-Theorem NZtimes_plus_distr_r : forall n m p : NZ, (n + m) * p == n * p + m * p.
+Theorem NZmul_add_distr_r : forall n m p : NZ, (n + m) * p == n * p + m * p.
 Proof.
 intros n m p; NZinduct n.
-rewrite NZtimes_0_l. now do 2 rewrite NZplus_0_l.
-intro n. rewrite NZplus_succ_l. do 2 rewrite NZtimes_succ_l.
-rewrite <- (NZplus_assoc (n * p) p (m * p)).
-rewrite (NZplus_comm p (m * p)). rewrite (NZplus_assoc (n * p) (m * p) p).
-now rewrite NZplus_cancel_r.
+rewrite NZmul_0_l. now do 2 rewrite NZadd_0_l.
+intro n. rewrite NZadd_succ_l. do 2 rewrite NZmul_succ_l.
+rewrite <- (NZadd_assoc (n * p) p (m * p)).
+rewrite (NZadd_comm p (m * p)). rewrite (NZadd_assoc (n * p) (m * p) p).
+now rewrite NZadd_cancel_r.
 Qed.
 
-Theorem NZtimes_plus_distr_l : forall n m p : NZ, n * (m + p) == n * m + n * p.
+Theorem NZmul_add_distr_l : forall n m p : NZ, n * (m + p) == n * m + n * p.
 Proof.
 intros n m p.
-rewrite (NZtimes_comm n (m + p)). rewrite (NZtimes_comm n m).
-rewrite (NZtimes_comm n p). apply NZtimes_plus_distr_r.
+rewrite (NZmul_comm n (m + p)). rewrite (NZmul_comm n m).
+rewrite (NZmul_comm n p). apply NZmul_add_distr_r.
 Qed.
 
-Theorem NZtimes_assoc : forall n m p : NZ, n * (m * p) == (n * m) * p.
+Theorem NZmul_assoc : forall n m p : NZ, n * (m * p) == (n * m) * p.
 Proof.
 intros n m p; NZinduct n.
-now do 3 rewrite NZtimes_0_l.
-intro n. do 2 rewrite NZtimes_succ_l. rewrite NZtimes_plus_distr_r.
-now rewrite NZplus_cancel_r.
+now do 3 rewrite NZmul_0_l.
+intro n. do 2 rewrite NZmul_succ_l. rewrite NZmul_add_distr_r.
+now rewrite NZadd_cancel_r.
 Qed.
 
-Theorem NZtimes_1_l : forall n : NZ, 1 * n == n.
+Theorem NZmul_1_l : forall n : NZ, 1 * n == n.
 Proof.
-intro n. rewrite NZtimes_succ_l; rewrite NZtimes_0_l. now rewrite NZplus_0_l.
+intro n. rewrite NZmul_succ_l; rewrite NZmul_0_l. now rewrite NZadd_0_l.
 Qed.
 
-Theorem NZtimes_1_r : forall n : NZ, n * 1 == n.
+Theorem NZmul_1_r : forall n : NZ, n * 1 == n.
 Proof.
-intro n; rewrite NZtimes_comm; apply NZtimes_1_l.
+intro n; rewrite NZmul_comm; apply NZmul_1_l.
 Qed.
 
 End NZTimesPropFunct.
diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v
index b48acc598..ebb2a9b5d 100644
--- a/theories/Numbers/NatInt/NZTimesOrder.v
+++ b/theories/Numbers/NatInt/NZTimesOrder.v
@@ -17,263 +17,263 @@ Module NZTimesOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig).
 Module Export NZPlusOrderPropMod := NZPlusOrderPropFunct NZOrdAxiomsMod.
 Open Local Scope NatIntScope.
 
-Theorem NZtimes_lt_pred :
+Theorem NZmul_lt_pred :
   forall p q n m : NZ, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
 Proof.
-intros p q n m H. rewrite <- H. do 2 rewrite NZtimes_succ_l.
-rewrite <- (NZplus_assoc (p * n) n m).
-rewrite <- (NZplus_assoc (p * m) m n).
-rewrite (NZplus_comm n m). now rewrite <- NZplus_lt_mono_r.
+intros p q n m H. rewrite <- H. do 2 rewrite NZmul_succ_l.
+rewrite <- (NZadd_assoc (p * n) n m).
+rewrite <- (NZadd_assoc (p * m) m n).
+rewrite (NZadd_comm n m). now rewrite <- NZadd_lt_mono_r.
 Qed.
 
-Theorem NZtimes_lt_mono_pos_l : forall p n m : NZ, 0 < p -> (n < m <-> p * n < p * m).
+Theorem NZmul_lt_mono_pos_l : forall p n m : NZ, 0 < p -> (n < m <-> p * n < p * m).
 Proof.
 NZord_induct p.
 intros n m H; false_hyp H NZlt_irrefl.
-intros p H IH n m H1. do 2 rewrite NZtimes_succ_l.
+intros p H IH n m H1. do 2 rewrite NZmul_succ_l.
 le_elim H. assert (LR : forall n m : NZ, n < m -> p * n + n < p * m + m).
-intros n1 m1 H2. apply NZplus_lt_mono; [now apply -> IH | assumption].
+intros n1 m1 H2. apply NZadd_lt_mono; [now apply -> IH | assumption].
 split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3.
 apply <- NZle_ngt in H3. le_elim H3.
 apply NZlt_asymm in H2. apply H2. now apply LR.
 rewrite H3 in H2; false_hyp H2 NZlt_irrefl.
-rewrite <- H; do 2 rewrite NZtimes_0_l; now do 2 rewrite NZplus_0_l.
+rewrite <- H; do 2 rewrite NZmul_0_l; now do 2 rewrite NZadd_0_l.
 intros p H1 _ n m H2. apply NZlt_asymm in H1. false_hyp H2 H1.
 Qed.
 
-Theorem NZtimes_lt_mono_pos_r : forall p n m : NZ, 0 < p -> (n < m <-> n * p < m * p).
+Theorem NZmul_lt_mono_pos_r : forall p n m : NZ, 0 < p -> (n < m <-> n * p < m * p).
 Proof.
 intros p n m.
-rewrite (NZtimes_comm n p); rewrite (NZtimes_comm m p). now apply NZtimes_lt_mono_pos_l.
+rewrite (NZmul_comm n p); rewrite (NZmul_comm m p). now apply NZmul_lt_mono_pos_l.
 Qed.
 
-Theorem NZtimes_lt_mono_neg_l : forall p n m : NZ, p < 0 -> (n < m <-> p * m < p * n).
+Theorem NZmul_lt_mono_neg_l : forall p n m : NZ, p < 0 -> (n < m <-> p * m < p * n).
 Proof.
 NZord_induct p.
 intros n m H; false_hyp H NZlt_irrefl.
 intros p H1 _ n m H2. apply NZlt_succ_l in H2. apply <- NZnle_gt in H2. false_hyp H1 H2.
 intros p H IH n m H1. apply <- NZle_succ_l in H.
 le_elim H. assert (LR : forall n m : NZ, n < m -> p * m < p * n).
-intros n1 m1 H2. apply (NZle_lt_plus_lt n1 m1).
-now apply NZlt_le_incl. do 2 rewrite <- NZtimes_succ_l. now apply -> IH.
+intros n1 m1 H2. apply (NZle_lt_add_lt n1 m1).
+now apply NZlt_le_incl. do 2 rewrite <- NZmul_succ_l. now apply -> IH.
 split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3.
 apply <- NZle_ngt in H3. le_elim H3.
 apply NZlt_asymm in H2. apply H2. now apply LR.
 rewrite H3 in H2; false_hyp H2 NZlt_irrefl.
-rewrite (NZtimes_lt_pred p (S p)) by reflexivity.
-rewrite H; do 2 rewrite NZtimes_0_l; now do 2 rewrite NZplus_0_l.
+rewrite (NZmul_lt_pred p (S p)) by reflexivity.
+rewrite H; do 2 rewrite NZmul_0_l; now do 2 rewrite NZadd_0_l.
 Qed.
 
-Theorem NZtimes_lt_mono_neg_r : forall p n m : NZ, p < 0 -> (n < m <-> m * p < n * p).
+Theorem NZmul_lt_mono_neg_r : forall p n m : NZ, p < 0 -> (n < m <-> m * p < n * p).
 Proof.
 intros p n m.
-rewrite (NZtimes_comm n p); rewrite (NZtimes_comm m p). now apply NZtimes_lt_mono_neg_l.
+rewrite (NZmul_comm n p); rewrite (NZmul_comm m p). now apply NZmul_lt_mono_neg_l.
 Qed.
 
-Theorem NZtimes_le_mono_nonneg_l : forall n m p : NZ, 0 <= p -> n <= m -> p * n <= p * m.
+Theorem NZmul_le_mono_nonneg_l : forall n m p : NZ, 0 <= p -> n <= m -> p * n <= p * m.
 Proof.
 intros n m p H1 H2. le_elim H1.
-le_elim H2. apply NZlt_le_incl. now apply -> NZtimes_lt_mono_pos_l.
+le_elim H2. apply NZlt_le_incl. now apply -> NZmul_lt_mono_pos_l.
 apply NZeq_le_incl; now rewrite H2.
-apply NZeq_le_incl; rewrite <- H1; now do 2 rewrite NZtimes_0_l.
+apply NZeq_le_incl; rewrite <- H1; now do 2 rewrite NZmul_0_l.
 Qed.
 
-Theorem NZtimes_le_mono_nonpos_l : forall n m p : NZ, p <= 0 -> n <= m -> p * m <= p * n.
+Theorem NZmul_le_mono_nonpos_l : forall n m p : NZ, p <= 0 -> n <= m -> p * m <= p * n.
 Proof.
 intros n m p H1 H2. le_elim H1.
-le_elim H2. apply NZlt_le_incl. now apply -> NZtimes_lt_mono_neg_l.
+le_elim H2. apply NZlt_le_incl. now apply -> NZmul_lt_mono_neg_l.
 apply NZeq_le_incl; now rewrite H2.
-apply NZeq_le_incl; rewrite H1; now do 2 rewrite NZtimes_0_l.
+apply NZeq_le_incl; rewrite H1; now do 2 rewrite NZmul_0_l.
 Qed.
 
-Theorem NZtimes_le_mono_nonneg_r : forall n m p : NZ, 0 <= p -> n <= m -> n * p <= m * p.
+Theorem NZmul_le_mono_nonneg_r : forall n m p : NZ, 0 <= p -> n <= m -> n * p <= m * p.
 Proof.
-intros n m p H1 H2; rewrite (NZtimes_comm n p); rewrite (NZtimes_comm m p);
-now apply NZtimes_le_mono_nonneg_l.
+intros n m p H1 H2; rewrite (NZmul_comm n p); rewrite (NZmul_comm m p);
+now apply NZmul_le_mono_nonneg_l.
 Qed.
 
-Theorem NZtimes_le_mono_nonpos_r : forall n m p : NZ, p <= 0 -> n <= m -> m * p <= n * p.
+Theorem NZmul_le_mono_nonpos_r : forall n m p : NZ, p <= 0 -> n <= m -> m * p <= n * p.
 Proof.
-intros n m p H1 H2; rewrite (NZtimes_comm n p); rewrite (NZtimes_comm m p);
-now apply NZtimes_le_mono_nonpos_l.
+intros n m p H1 H2; rewrite (NZmul_comm n p); rewrite (NZmul_comm m p);
+now apply NZmul_le_mono_nonpos_l.
 Qed.
 
-Theorem NZtimes_cancel_l : forall n m p : NZ, p ~= 0 -> (p * n == p * m <-> n == m).
+Theorem NZmul_cancel_l : forall n m p : NZ, p ~= 0 -> (p * n == p * m <-> n == m).
 Proof.
 intros n m p H; split; intro H1.
 destruct (NZlt_trichotomy p 0) as [H2 | [H2 | H2]].
 apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3].
-assert (H4 : p * m < p * n); [now apply -> NZtimes_lt_mono_neg_l |].
+assert (H4 : p * m < p * n); [now apply -> NZmul_lt_mono_neg_l |].
 rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
-assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_neg_l |].
+assert (H4 : p * n < p * m); [now apply -> NZmul_lt_mono_neg_l |].
 rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
 false_hyp H2 H.
 apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3].
-assert (H4 : p * n < p * m) by (now apply -> NZtimes_lt_mono_pos_l).
+assert (H4 : p * n < p * m) by (now apply -> NZmul_lt_mono_pos_l).
 rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
-assert (H4 : p * m < p * n) by (now apply -> NZtimes_lt_mono_pos_l).
+assert (H4 : p * m < p * n) by (now apply -> NZmul_lt_mono_pos_l).
 rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
 now rewrite H1.
 Qed.
 
-Theorem NZtimes_cancel_r : forall n m p : NZ, p ~= 0 -> (n * p == m * p <-> n == m).
+Theorem NZmul_cancel_r : forall n m p : NZ, p ~= 0 -> (n * p == m * p <-> n == m).
 Proof.
-intros n m p. rewrite (NZtimes_comm n p), (NZtimes_comm m p); apply NZtimes_cancel_l.
+intros n m p. rewrite (NZmul_comm n p), (NZmul_comm m p); apply NZmul_cancel_l.
 Qed.
 
-Theorem NZtimes_id_l : forall n m : NZ, m ~= 0 -> (n * m == m <-> n == 1).
+Theorem NZmul_id_l : forall n m : NZ, m ~= 0 -> (n * m == m <-> n == 1).
 Proof.
 intros n m H.
-stepl (n * m == 1 * m) by now rewrite NZtimes_1_l. now apply NZtimes_cancel_r.
+stepl (n * m == 1 * m) by now rewrite NZmul_1_l. now apply NZmul_cancel_r.
 Qed.
 
-Theorem NZtimes_id_r : forall n m : NZ, n ~= 0 -> (n * m == n <-> m == 1).
+Theorem NZmul_id_r : forall n m : NZ, n ~= 0 -> (n * m == n <-> m == 1).
 Proof.
-intros n m; rewrite NZtimes_comm; apply NZtimes_id_l.
+intros n m; rewrite NZmul_comm; apply NZmul_id_l.
 Qed.
 
-Theorem NZtimes_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m).
+Theorem NZmul_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m).
 Proof.
 intros n m p H; do 2 rewrite NZlt_eq_cases.
-rewrite (NZtimes_lt_mono_pos_l p n m) by assumption.
-now rewrite -> (NZtimes_cancel_l n m p) by
+rewrite (NZmul_lt_mono_pos_l p n m) by assumption.
+now rewrite -> (NZmul_cancel_l n m p) by
 (intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl).
 Qed.
 
-Theorem NZtimes_le_mono_pos_r : forall n m p : NZ, 0 < p -> (n <= m <-> n * p <= m * p).
+Theorem NZmul_le_mono_pos_r : forall n m p : NZ, 0 < p -> (n <= m <-> n * p <= m * p).
 Proof.
-intros n m p. rewrite (NZtimes_comm n p); rewrite (NZtimes_comm m p);
-apply NZtimes_le_mono_pos_l.
+intros n m p. rewrite (NZmul_comm n p); rewrite (NZmul_comm m p);
+apply NZmul_le_mono_pos_l.
 Qed.
 
-Theorem NZtimes_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n).
+Theorem NZmul_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n).
 Proof.
 intros n m p H; do 2 rewrite NZlt_eq_cases.
-rewrite (NZtimes_lt_mono_neg_l p n m); [| assumption].
-rewrite -> (NZtimes_cancel_l m n p) by (intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl).
+rewrite (NZmul_lt_mono_neg_l p n m); [| assumption].
+rewrite -> (NZmul_cancel_l m n p) by (intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl).
 now setoid_replace (n == m) with (m == n) using relation iff by (split; now intro).
 Qed.
 
-Theorem NZtimes_le_mono_neg_r : forall n m p : NZ, p < 0 -> (n <= m <-> m * p <= n * p).
+Theorem NZmul_le_mono_neg_r : forall n m p : NZ, p < 0 -> (n <= m <-> m * p <= n * p).
 Proof.
-intros n m p. rewrite (NZtimes_comm n p); rewrite (NZtimes_comm m p);
-apply NZtimes_le_mono_neg_l.
+intros n m p. rewrite (NZmul_comm n p); rewrite (NZmul_comm m p);
+apply NZmul_le_mono_neg_l.
 Qed.
 
-Theorem NZtimes_lt_mono_nonneg :
+Theorem NZmul_lt_mono_nonneg :
   forall n m p q : NZ, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q.
 Proof.
 intros n m p q H1 H2 H3 H4.
 apply NZle_lt_trans with (m * p).
-apply NZtimes_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl].
-apply -> NZtimes_lt_mono_pos_l; [assumption | now apply NZle_lt_trans with n].
+apply NZmul_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl].
+apply -> NZmul_lt_mono_pos_l; [assumption | now apply NZle_lt_trans with n].
 Qed.
 
 (* There are still many variants of the theorem above. One can assume 0 < n
 or 0 < p or n <= m or p <= q. *)
 
-Theorem NZtimes_le_mono_nonneg :
+Theorem NZmul_le_mono_nonneg :
   forall n m p q : NZ, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q.
 Proof.
 intros n m p q H1 H2 H3 H4.
 le_elim H2; le_elim H4.
-apply NZlt_le_incl; now apply NZtimes_lt_mono_nonneg.
-rewrite <- H4; apply NZtimes_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl].
-rewrite <- H2; apply NZtimes_le_mono_nonneg_l; [assumption | now apply NZlt_le_incl].
+apply NZlt_le_incl; now apply NZmul_lt_mono_nonneg.
+rewrite <- H4; apply NZmul_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl].
+rewrite <- H2; apply NZmul_le_mono_nonneg_l; [assumption | now apply NZlt_le_incl].
 rewrite H2; rewrite H4; now apply NZeq_le_incl.
 Qed.
 
-Theorem NZtimes_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n * m.
+Theorem NZmul_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n * m.
 Proof.
 intros n m H1 H2.
-rewrite <- (NZtimes_0_l m). now apply -> NZtimes_lt_mono_pos_r.
+rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_pos_r.
 Qed.
 
-Theorem NZtimes_neg_neg : forall n m : NZ, n < 0 -> m < 0 -> 0 < n * m.
+Theorem NZmul_neg_neg : forall n m : NZ, n < 0 -> m < 0 -> 0 < n * m.
 Proof.
 intros n m H1 H2.
-rewrite <- (NZtimes_0_l m). now apply -> NZtimes_lt_mono_neg_r.
+rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_neg_r.
 Qed.
 
-Theorem NZtimes_pos_neg : forall n m : NZ, 0 < n -> m < 0 -> n * m < 0.
+Theorem NZmul_pos_neg : forall n m : NZ, 0 < n -> m < 0 -> n * m < 0.
 Proof.
 intros n m H1 H2.
-rewrite <- (NZtimes_0_l m). now apply -> NZtimes_lt_mono_neg_r.
+rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_neg_r.
 Qed.
 
-Theorem NZtimes_neg_pos : forall n m : NZ, n < 0 -> 0 < m -> n * m < 0.
+Theorem NZmul_neg_pos : forall n m : NZ, n < 0 -> 0 < m -> n * m < 0.
 Proof.
-intros; rewrite NZtimes_comm; now apply NZtimes_pos_neg.
+intros; rewrite NZmul_comm; now apply NZmul_pos_neg.
 Qed.
 
-Theorem NZlt_1_times_pos : forall n m : NZ, 1 < n -> 0 < m -> 1 < n * m.
+Theorem NZlt_1_mul_pos : forall n m : NZ, 1 < n -> 0 < m -> 1 < n * m.
 Proof.
-intros n m H1 H2. apply -> (NZtimes_lt_mono_pos_r m) in H1.
-rewrite NZtimes_1_l in H1. now apply NZlt_1_l with m.
+intros n m H1 H2. apply -> (NZmul_lt_mono_pos_r m) in H1.
+rewrite NZmul_1_l in H1. now apply NZlt_1_l with m.
 assumption.
 Qed.
 
-Theorem NZeq_times_0 : forall n m : NZ, n * m == 0 <-> n == 0 \/ m == 0.
+Theorem NZeq_mul_0 : forall n m : NZ, n * m == 0 <-> n == 0 \/ m == 0.
 Proof.
 intros n m; split.
 intro H; destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]];
 destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]];
 try (now right); try (now left).
-elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZtimes_neg_neg |].
-elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZtimes_neg_pos |].
-elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZtimes_pos_neg |].
-elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZtimes_pos_pos |].
-intros [H | H]. now rewrite H, NZtimes_0_l. now rewrite H, NZtimes_0_r.
+elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZmul_neg_neg |].
+elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZmul_neg_pos |].
+elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZmul_pos_neg |].
+elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZmul_pos_pos |].
+intros [H | H]. now rewrite H, NZmul_0_l. now rewrite H, NZmul_0_r.
 Qed.
 
-Theorem NZneq_times_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
+Theorem NZneq_mul_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
 Proof.
 intros n m; split; intro H.
-intro H1; apply -> NZeq_times_0 in H1. tauto.
+intro H1; apply -> NZeq_mul_0 in H1. tauto.
 split; intro H1; rewrite H1 in H;
-(rewrite NZtimes_0_l in H || rewrite NZtimes_0_r in H); now apply H.
+(rewrite NZmul_0_l in H || rewrite NZmul_0_r in H); now apply H.
 Qed.
 
 Theorem NZeq_square_0 : forall n : NZ, n * n == 0 <-> n == 0.
 Proof.
-intro n; rewrite NZeq_times_0; tauto.
+intro n; rewrite NZeq_mul_0; tauto.
 Qed.
 
-Theorem NZeq_times_0_l : forall n m : NZ, n * m == 0 -> m ~= 0 -> n == 0.
+Theorem NZeq_mul_0_l : forall n m : NZ, n * m == 0 -> m ~= 0 -> n == 0.
 Proof.
-intros n m H1 H2. apply -> NZeq_times_0 in H1. destruct H1 as [H1 | H1].
+intros n m H1 H2. apply -> NZeq_mul_0 in H1. destruct H1 as [H1 | H1].
 assumption. false_hyp H1 H2.
 Qed.
 
-Theorem NZeq_times_0_r : forall n m : NZ, n * m == 0 -> n ~= 0 -> m == 0.
+Theorem NZeq_mul_0_r : forall n m : NZ, n * m == 0 -> n ~= 0 -> m == 0.
 Proof.
-intros n m H1 H2; apply -> NZeq_times_0 in H1. destruct H1 as [H1 | H1].
+intros n m H1 H2; apply -> NZeq_mul_0 in H1. destruct H1 as [H1 | H1].
 false_hyp H1 H2. assumption.
 Qed.
 
-Theorem NZlt_0_times : forall n m : NZ, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0).
+Theorem NZlt_0_mul : forall n m : NZ, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0).
 Proof.
 intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]].
 destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]];
-[| rewrite H1 in H; rewrite NZtimes_0_l in H; false_hyp H NZlt_irrefl |];
+[| rewrite H1 in H; rewrite NZmul_0_l in H; false_hyp H NZlt_irrefl |];
 (destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]];
-[| rewrite H2 in H; rewrite NZtimes_0_r in H; false_hyp H NZlt_irrefl |]);
+[| rewrite H2 in H; rewrite NZmul_0_r in H; false_hyp H NZlt_irrefl |]);
 try (left; now split); try (right; now split).
-assert (H3 : n * m < 0) by now apply NZtimes_neg_pos.
+assert (H3 : n * m < 0) by now apply NZmul_neg_pos.
 elimtype False; now apply (NZlt_asymm (n * m) 0).
-assert (H3 : n * m < 0) by now apply NZtimes_pos_neg.
+assert (H3 : n * m < 0) by now apply NZmul_pos_neg.
 elimtype False; now apply (NZlt_asymm (n * m) 0).
-now apply NZtimes_pos_pos. now apply NZtimes_neg_neg.
+now apply NZmul_pos_pos. now apply NZmul_neg_neg.
 Qed.
 
 Theorem NZsquare_lt_mono_nonneg : forall n m : NZ, 0 <= n -> n < m -> n * n < m * m.
 Proof.
-intros n m H1 H2. now apply NZtimes_lt_mono_nonneg.
+intros n m H1 H2. now apply NZmul_lt_mono_nonneg.
 Qed.
 
 Theorem NZsquare_le_mono_nonneg : forall n m : NZ, 0 <= n -> n <= m -> n * n <= m * m.
 Proof.
-intros n m H1 H2. now apply NZtimes_le_mono_nonneg.
+intros n m H1 H2. now apply NZmul_le_mono_nonneg.
 Qed.
 
 (* The converse theorems require nonnegativity (or nonpositivity) of the
@@ -297,14 +297,14 @@ assumption. assert (F : m * m < n * n) by now apply NZsquare_lt_mono_nonneg.
 apply -> NZlt_nge in F. false_hyp H2 F.
 Qed.
 
-Theorem NZtimes_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
+Theorem NZmul_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
 Proof.
 intros n m H. apply <- NZle_succ_l in H.
-apply -> (NZtimes_le_mono_pos_l (S n) m (1 + 1)) in H.
-repeat rewrite NZtimes_plus_distr_r in *; repeat rewrite NZtimes_1_l in *.
-repeat rewrite NZplus_succ_r in *. repeat rewrite NZplus_succ_l in *. rewrite NZplus_0_l.
+apply -> (NZmul_le_mono_pos_l (S n) m (1 + 1)) in H.
+repeat rewrite NZmul_add_distr_r in *; repeat rewrite NZmul_1_l in *.
+repeat rewrite NZadd_succ_r in *. repeat rewrite NZadd_succ_l in *. rewrite NZadd_0_l.
 now apply -> NZle_succ_l.
-apply NZplus_pos_pos; now apply NZlt_succ_diag_r.
+apply NZadd_pos_pos; now apply NZlt_succ_diag_r.
 Qed.
 
 End NZTimesOrderPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index a4e8c056f..c31f216a3 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -24,8 +24,8 @@ Notation N0 := NZ0.
 Notation N1 := (NZsucc NZ0).
 Notation S := NZsucc.
 Notation P := NZpred.
-Notation plus := NZplus.
-Notation times := NZtimes.
+Notation add := NZadd.
+Notation mul := NZmul.
 Notation minus := NZminus.
 Notation lt := NZlt.
 Notation le := NZle.
@@ -35,9 +35,9 @@ Notation "x == y"  := (Neq x y) (at level 70) : NatScope.
 Notation "x ~= y" := (~ Neq x y) (at level 70) : NatScope.
 Notation "0" := NZ0 : NatScope.
 Notation "1" := (NZsucc NZ0) : NatScope.
-Notation "x + y" := (NZplus x y) : NatScope.
+Notation "x + y" := (NZadd x y) : NatScope.
 Notation "x - y" := (NZminus x y) : NatScope.
-Notation "x * y" := (NZtimes x y) : NatScope.
+Notation "x * y" := (NZmul x y) : NatScope.
 Notation "x < y" := (NZlt x y) : NatScope.
 Notation "x <= y" := (NZle x y) : NatScope.
 Notation "x > y" := (NZlt y x) (only parsing) : NatScope.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index e90977e3d..eb46e69de 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -25,12 +25,12 @@ only one time. *)
 Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod.
 
 (* Here we probably need to re-prove all axioms declared in NAxioms.v to
-make sure that the definitions like N, S and plus are unfolded in them,
+make sure that the definitions like N, S and add are unfolded in them,
 since unfolding is done only inside a functor. In fact, we'll do it in the
 files that prove the corresponding properties. In those files, we will also
 rename properties proved in NZ files by removing NZ from their names. In
 this way, one only has to consult, for example, NPlus.v to see all
-available properties for plus, i.e., one does not have to go to NAxioms.v
+available properties for add, i.e., one does not have to go to NAxioms.v
 for axioms and NZPlus.v for theorems. *)
 
 Theorem succ_wd : forall n1 n2 : N, n1 == n2 -> S n1 == S n2.
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 369c1261c..57d33e7b6 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -20,13 +20,13 @@ Open Local Scope NatScope.
 (*****************************************************)
 (**                   Addition                       *)
 
-Definition def_plus (x y : N) := recursion y (fun _ p => S p) x.
+Definition def_add (x y : N) := recursion y (fun _ p => S p) x.
 
-Infix Local "++" := def_plus (at level 50, left associativity).
+Infix Local "++" := def_add (at level 50, left associativity).
 
-Add Morphism def_plus with signature Neq ==> Neq ==> Neq as def_plus_wd.
+Add Morphism def_add with signature Neq ==> Neq ==> Neq as def_add_wd.
 Proof.
-unfold def_plus.
+unfold def_add.
 intros x x' Exx' y y' Eyy'.
 apply recursion_wd with (Aeq := Neq).
 assumption.
@@ -34,68 +34,68 @@ unfold fun2_eq; intros _ _ _ p p' Epp'; now rewrite Epp'.
 assumption.
 Qed.
 
-Theorem def_plus_0_l : forall y : N, 0 ++ y == y.
+Theorem def_add_0_l : forall y : N, 0 ++ y == y.
 Proof.
-intro y. unfold def_plus. now rewrite recursion_0.
+intro y. unfold def_add. now rewrite recursion_0.
 Qed.
 
-Theorem def_plus_succ_l : forall x y : N, S x ++ y == S (x ++ y).
+Theorem def_add_succ_l : forall x y : N, S x ++ y == S (x ++ y).
 Proof.
-intros x y; unfold def_plus.
+intros x y; unfold def_add.
 rewrite (@recursion_succ N Neq); try reflexivity.
 unfold fun2_wd. intros _ _ _ m1 m2 H2. now rewrite H2.
 Qed.
 
-Theorem def_plus_plus : forall n m : N, n ++ m == n + m.
+Theorem def_add_add : forall n m : N, n ++ m == n + m.
 Proof.
 intros n m; induct n.
-now rewrite def_plus_0_l, plus_0_l.
-intros n H. now rewrite def_plus_succ_l, plus_succ_l, H.
+now rewrite def_add_0_l, add_0_l.
+intros n H. now rewrite def_add_succ_l, add_succ_l, H.
 Qed.
 
 (*****************************************************)
 (**                  Multiplication                  *)
 
-Definition def_times (x y : N) := recursion 0 (fun _ p => p ++ x) y.
+Definition def_mul (x y : N) := recursion 0 (fun _ p => p ++ x) y.
 
-Infix Local "**" := def_times (at level 40, left associativity).
+Infix Local "**" := def_mul (at level 40, left associativity).
 
-Lemma def_times_step_wd : forall x : N, fun2_wd Neq Neq Neq (fun _ p => def_plus p x).
+Lemma def_mul_step_wd : forall x : N, fun2_wd Neq Neq Neq (fun _ p => def_add p x).
 Proof.
-unfold fun2_wd. intros. now apply def_plus_wd.
+unfold fun2_wd. intros. now apply def_add_wd.
 Qed.
 
-Lemma def_times_step_equal :
+Lemma def_mul_step_equal :
   forall x x' : N, x == x' ->
-    fun2_eq Neq Neq Neq (fun _ p => def_plus p x) (fun x p => def_plus p x').
+    fun2_eq Neq Neq Neq (fun _ p => def_add p x) (fun x p => def_add p x').
 Proof.
-unfold fun2_eq; intros; apply def_plus_wd; assumption.
+unfold fun2_eq; intros; apply def_add_wd; assumption.
 Qed.
 
-Add Morphism def_times with signature Neq ==> Neq ==> Neq as def_times_wd.
+Add Morphism def_mul with signature Neq ==> Neq ==> Neq as def_mul_wd.
 Proof.
-unfold def_times.
+unfold def_mul.
 intros x x' Exx' y y' Eyy'.
 apply recursion_wd with (Aeq := Neq).
-reflexivity. apply def_times_step_equal. assumption. assumption.
+reflexivity. apply def_mul_step_equal. assumption. assumption.
 Qed.
 
-Theorem def_times_0_r : forall x : N, x ** 0 == 0.
+Theorem def_mul_0_r : forall x : N, x ** 0 == 0.
 Proof.
-intro. unfold def_times. now rewrite recursion_0.
+intro. unfold def_mul. now rewrite recursion_0.
 Qed.
 
-Theorem def_times_succ_r : forall x y : N, x ** S y == x ** y ++ x.
+Theorem def_mul_succ_r : forall x y : N, x ** S y == x ** y ++ x.
 Proof.
-intros x y; unfold def_times.
-now rewrite (@recursion_succ N Neq); [| apply def_times_step_wd |].
+intros x y; unfold def_mul.
+now rewrite (@recursion_succ N Neq); [| apply def_mul_step_wd |].
 Qed.
 
-Theorem def_times_times : forall n m : N, n ** m == n * m.
+Theorem def_mul_mul : forall n m : N, n ** m == n * m.
 Proof.
 intros n m; induct m.
-now rewrite def_times_0_r, times_0_r.
-intros m IH; now rewrite def_times_succ_r, times_succ_r, def_plus_plus, IH.
+now rewrite def_mul_0_r, mul_0_r.
+intros m IH; now rewrite def_mul_succ_r, mul_succ_r, def_add_add, IH.
 Qed.
 
 (*****************************************************)
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index 0c24ca984..81b41dc03 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -58,71 +58,71 @@ intro; rewrite minus_0_r; apply neq_succ_0.
 intros; now rewrite minus_succ.
 Qed.
 
-Theorem plus_minus_assoc : forall n m p : N, p <= m -> n + (m - p) == (n + m) - p.
+Theorem add_minus_assoc : forall n m p : N, p <= m -> n + (m - p) == (n + m) - p.
 Proof.
 intros n m p; induct p.
 intro; now do 2 rewrite minus_0_r.
 intros p IH H. do 2 rewrite minus_succ_r.
 rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l).
-rewrite plus_pred_r by (apply minus_gt; now apply -> le_succ_l).
+rewrite add_pred_r by (apply minus_gt; now apply -> le_succ_l).
 reflexivity.
 Qed.
 
 Theorem minus_succ_l : forall n m : N, n <= m -> S m - n == S (m - n).
 Proof.
-intros n m H. rewrite <- (plus_1_l m). rewrite <- (plus_1_l (m - n)).
-symmetry; now apply plus_minus_assoc.
+intros n m H. rewrite <- (add_1_l m). rewrite <- (add_1_l (m - n)).
+symmetry; now apply add_minus_assoc.
 Qed.
 
-Theorem plus_minus : forall n m : N, (n + m) - m == n.
+Theorem add_minus : forall n m : N, (n + m) - m == n.
 Proof.
-intros n m. rewrite <- plus_minus_assoc by (apply le_refl).
-rewrite minus_diag; now rewrite plus_0_r.
+intros n m. rewrite <- add_minus_assoc by (apply le_refl).
+rewrite minus_diag; now rewrite add_0_r.
 Qed.
 
-Theorem minus_plus : forall n m : N, n <= m -> (m - n) + n == m.
+Theorem minus_add : forall n m : N, n <= m -> (m - n) + n == m.
 Proof.
-intros n m H. rewrite plus_comm. rewrite plus_minus_assoc by assumption.
-rewrite plus_comm. apply plus_minus.
+intros n m H. rewrite add_comm. rewrite add_minus_assoc by assumption.
+rewrite add_comm. apply add_minus.
 Qed.
 
-Theorem plus_minus_eq_l : forall n m p : N, m + p == n -> n - m == p.
+Theorem add_minus_eq_l : forall n m p : N, m + p == n -> n - m == p.
 Proof.
 intros n m p H. symmetry.
 assert (H1 : m + p - m == n - m) by now rewrite H.
-rewrite plus_comm in H1. now rewrite plus_minus in H1.
+rewrite add_comm in H1. now rewrite add_minus in H1.
 Qed.
 
-Theorem plus_minus_eq_r : forall n m p : N, m + p == n -> n - p == m.
+Theorem add_minus_eq_r : forall n m p : N, m + p == n -> n - p == m.
 Proof.
-intros n m p H; rewrite plus_comm in H; now apply plus_minus_eq_l.
+intros n m p H; rewrite add_comm in H; now apply add_minus_eq_l.
 Qed.
 
 (* This could be proved by adding m to both sides. Then the proof would
-use plus_minus_assoc and minus_0_le, which is proven below. *)
+use add_minus_assoc and minus_0_le, which is proven below. *)
 
-Theorem plus_minus_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n.
+Theorem add_minus_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n.
 Proof.
 intros n m p H; double_induct n m.
 intros m H1; rewrite minus_0_l in H1. symmetry in H1; false_hyp H1 H.
-intro n; rewrite minus_0_r; now rewrite plus_0_l.
+intro n; rewrite minus_0_r; now rewrite add_0_l.
 intros n m IH H1. rewrite minus_succ in H1. apply IH in H1.
-rewrite plus_succ_l; now rewrite H1.
+rewrite add_succ_l; now rewrite H1.
 Qed.
 
-Theorem minus_plus_distr : forall n m p : N, n - (m + p) == (n - m) - p.
+Theorem minus_add_distr : forall n m p : N, n - (m + p) == (n - m) - p.
 Proof.
 intros n m; induct p.
-rewrite plus_0_r; now rewrite minus_0_r.
-intros p IH. rewrite plus_succ_r; do 2 rewrite minus_succ_r. now rewrite IH.
+rewrite add_0_r; now rewrite minus_0_r.
+intros p IH. rewrite add_succ_r; do 2 rewrite minus_succ_r. now rewrite IH.
 Qed.
 
-Theorem plus_minus_swap : forall n m p : N, p <= n -> n + m - p == n - p + m.
+Theorem add_minus_swap : forall n m p : N, p <= n -> n + m - p == n - p + m.
 Proof.
 intros n m p H.
-rewrite (plus_comm n m).
-rewrite <- plus_minus_assoc by assumption.
-now rewrite (plus_comm m (n - p)).
+rewrite (add_comm n m).
+rewrite <- add_minus_assoc by assumption.
+now rewrite (add_comm m (n - p)).
 Qed.
 
 (** Minus and order *)
@@ -144,36 +144,36 @@ intro m; rewrite minus_0_r; split; intro H;
 intros n m H. rewrite <- succ_le_mono. now rewrite minus_succ.
 Qed.
 
-(** Minus and times *)
+(** Minus and mul *)
 
-Theorem times_pred_r : forall n m : N, n * (P m) == n * m - n.
+Theorem mul_pred_r : forall n m : N, n * (P m) == n * m - n.
 Proof.
 intros n m; cases m.
-now rewrite pred_0, times_0_r, minus_0_l.
-intro m; rewrite pred_succ, times_succ_r, <- plus_minus_assoc.
-now rewrite minus_diag, plus_0_r.
+now rewrite pred_0, mul_0_r, minus_0_l.
+intro m; rewrite pred_succ, mul_succ_r, <- add_minus_assoc.
+now rewrite minus_diag, add_0_r.
 now apply eq_le_incl.
 Qed.
 
-Theorem times_minus_distr_r : forall n m p : N, (n - m) * p == n * p - m * p.
+Theorem mul_minus_distr_r : forall n m p : N, (n - m) * p == n * p - m * p.
 Proof.
 intros n m p; induct n.
-now rewrite minus_0_l, times_0_l, minus_0_l.
+now rewrite minus_0_l, mul_0_l, minus_0_l.
 intros n IH. destruct (le_gt_cases m n) as [H | H].
-rewrite minus_succ_l by assumption. do 2 rewrite times_succ_l.
-rewrite (plus_comm ((n - m) * p) p), (plus_comm (n * p) p).
-rewrite <- (plus_minus_assoc p (n * p) (m * p)) by now apply times_le_mono_r.
-now apply <- plus_cancel_l.
+rewrite minus_succ_l by assumption. do 2 rewrite mul_succ_l.
+rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p).
+rewrite <- (add_minus_assoc p (n * p) (m * p)) by now apply mul_le_mono_r.
+now apply <- add_cancel_l.
 assert (H1 : S n <= m); [now apply <- le_succ_l |].
 setoid_replace (S n - m) with 0 by now apply <- minus_0_le.
-setoid_replace ((S n * p) - m * p) with 0 by (apply <- minus_0_le; now apply times_le_mono_r).
-apply times_0_l.
+setoid_replace ((S n * p) - m * p) with 0 by (apply <- minus_0_le; now apply mul_le_mono_r).
+apply mul_0_l.
 Qed.
 
-Theorem times_minus_distr_l : forall n m p : N, p * (n - m) == p * n - p * m.
+Theorem mul_minus_distr_l : forall n m p : N, p * (n - m) == p * n - p * m.
 Proof.
-intros n m p; rewrite (times_comm p (n - m)), (times_comm p n), (times_comm p m).
-apply times_minus_distr_r.
+intros n m p; rewrite (mul_comm p (n - m)), (mul_comm p n), (mul_comm p m).
+apply mul_minus_distr_r.
 Qed.
 
 End NMinusPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v
index 71122e3a5..67443acff 100644
--- a/theories/Numbers/Natural/Abstract/NPlus.v
+++ b/theories/Numbers/Natural/Abstract/NPlus.v
@@ -17,108 +17,108 @@ Module Export NBasePropMod := NBasePropFunct NAxiomsMod.
 
 Open Local Scope NatScope.
 
-Theorem plus_wd :
+Theorem add_wd :
   forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 + m1 == n2 + m2.
-Proof NZplus_wd.
+Proof NZadd_wd.
 
-Theorem plus_0_l : forall n : N, 0 + n == n.
-Proof NZplus_0_l.
+Theorem add_0_l : forall n : N, 0 + n == n.
+Proof NZadd_0_l.
 
-Theorem plus_succ_l : forall n m : N, (S n) + m == S (n + m).
-Proof NZplus_succ_l.
+Theorem add_succ_l : forall n m : N, (S n) + m == S (n + m).
+Proof NZadd_succ_l.
 
 (** Theorems that are valid for both natural numbers and integers *)
 
-Theorem plus_0_r : forall n : N, n + 0 == n.
-Proof NZplus_0_r.
+Theorem add_0_r : forall n : N, n + 0 == n.
+Proof NZadd_0_r.
 
-Theorem plus_succ_r : forall n m : N, n + S m == S (n + m).
-Proof NZplus_succ_r.
+Theorem add_succ_r : forall n m : N, n + S m == S (n + m).
+Proof NZadd_succ_r.
 
-Theorem plus_comm : forall n m : N, n + m == m + n.
-Proof NZplus_comm.
+Theorem add_comm : forall n m : N, n + m == m + n.
+Proof NZadd_comm.
 
-Theorem plus_assoc : forall n m p : N, n + (m + p) == (n + m) + p.
-Proof NZplus_assoc.
+Theorem add_assoc : forall n m p : N, n + (m + p) == (n + m) + p.
+Proof NZadd_assoc.
 
-Theorem plus_shuffle1 : forall n m p q : N, (n + m) + (p + q) == (n + p) + (m + q).
-Proof NZplus_shuffle1.
+Theorem add_shuffle1 : forall n m p q : N, (n + m) + (p + q) == (n + p) + (m + q).
+Proof NZadd_shuffle1.
 
-Theorem plus_shuffle2 : forall n m p q : N, (n + m) + (p + q) == (n + q) + (m + p).
-Proof NZplus_shuffle2.
+Theorem add_shuffle2 : forall n m p q : N, (n + m) + (p + q) == (n + q) + (m + p).
+Proof NZadd_shuffle2.
 
-Theorem plus_1_l : forall n : N, 1 + n == S n.
-Proof NZplus_1_l.
+Theorem add_1_l : forall n : N, 1 + n == S n.
+Proof NZadd_1_l.
 
-Theorem plus_1_r : forall n : N, n + 1 == S n.
-Proof NZplus_1_r.
+Theorem add_1_r : forall n : N, n + 1 == S n.
+Proof NZadd_1_r.
 
-Theorem plus_cancel_l : forall n m p : N, p + n == p + m <-> n == m.
-Proof NZplus_cancel_l.
+Theorem add_cancel_l : forall n m p : N, p + n == p + m <-> n == m.
+Proof NZadd_cancel_l.
 
-Theorem plus_cancel_r : forall n m p : N, n + p == m + p <-> n == m.
-Proof NZplus_cancel_r.
+Theorem add_cancel_r : forall n m p : N, n + p == m + p <-> n == m.
+Proof NZadd_cancel_r.
 
 (* Theorems that are valid for natural numbers but cannot be proved for Z *)
 
-Theorem eq_plus_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0.
+Theorem eq_add_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0.
 Proof.
 intros n m; induct n.
-(* The next command does not work with the axiom plus_0_l from NPlusSig *)
-rewrite plus_0_l. intuition reflexivity.
-intros n IH. rewrite plus_succ_l.
+(* The next command does not work with the axiom add_0_l from NPlusSig *)
+rewrite add_0_l. intuition reflexivity.
+intros n IH. rewrite add_succ_l.
 setoid_replace (S (n + m) == 0) with False using relation iff by
  (apply -> neg_false; apply neq_succ_0).
 setoid_replace (S n == 0) with False using relation iff by
  (apply -> neg_false; apply neq_succ_0). tauto.
 Qed.
 
-Theorem eq_plus_succ :
+Theorem eq_add_succ :
   forall n m : N, (exists p : N, n + m == S p) <->
                     (exists n' : N, n == S n') \/ (exists m' : N, m == S m').
 Proof.
 intros n m; cases n.
 split; intro H.
-destruct H as [p H]. rewrite plus_0_l in H; right; now exists p.
+destruct H as [p H]. rewrite add_0_l in H; right; now exists p.
 destruct H as [[n' H] | [m' H]].
 symmetry in H; false_hyp H neq_succ_0.
-exists m'; now rewrite plus_0_l.
+exists m'; now rewrite add_0_l.
 intro n; split; intro H.
 left; now exists n.
-exists (n + m); now rewrite plus_succ_l.
+exists (n + m); now rewrite add_succ_l.
 Qed.
 
-Theorem eq_plus_1 : forall n m : N,
+Theorem eq_add_1 : forall n m : N,
   n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1.
 Proof.
 intros n m H.
 assert (H1 : exists p : N, n + m == S p) by now exists 0.
-apply -> eq_plus_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
-left. rewrite H1 in H; rewrite plus_succ_l in H; apply succ_inj in H.
-apply -> eq_plus_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split.
-right. rewrite H1 in H; rewrite plus_succ_r in H; apply succ_inj in H.
-apply -> eq_plus_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split.
+apply -> eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
+left. rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H.
+apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split.
+right. rewrite H1 in H; rewrite add_succ_r in H; apply succ_inj in H.
+apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split.
 Qed.
 
-Theorem succ_plus_discr : forall n m : N, m ~= S (n + m).
+Theorem succ_add_discr : forall n m : N, m ~= S (n + m).
 Proof.
 intro n; induct m.
 apply neq_symm. apply neq_succ_0.
-intros m IH H. apply succ_inj in H. rewrite plus_succ_r in H.
+intros m IH H. apply succ_inj in H. rewrite add_succ_r in H.
 unfold not in IH; now apply IH.
 Qed.
 
-Theorem plus_pred_l : forall n m : N, n ~= 0 -> P n + m == P (n + m).
+Theorem add_pred_l : forall n m : N, n ~= 0 -> P n + m == P (n + m).
 Proof.
 intros n m; cases n.
 intro H; now elim H.
-intros n IH; rewrite plus_succ_l; now do 2 rewrite pred_succ.
+intros n IH; rewrite add_succ_l; now do 2 rewrite pred_succ.
 Qed.
 
-Theorem plus_pred_r : forall n m : N, m ~= 0 -> n + P m == P (n + m).
+Theorem add_pred_r : forall n m : N, m ~= 0 -> n + P m == P (n + m).
 Proof.
-intros n m H; rewrite (plus_comm n (P m));
-rewrite (plus_comm n m); now apply plus_pred_l.
+intros n m H; rewrite (add_comm n (P m));
+rewrite (add_comm n m); now apply add_pred_l.
 Qed.
 
 (* One could define n <= m as exists p : N, p + n == m. Then we have
@@ -133,23 +133,23 @@ forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n)     (1)
 We will need (1) in the proof of induction principle for integers
 constructed as pairs of natural numbers. The formula (1) can be proved
 using properties of order and truncated subtraction. Thus, p would be
-m - n or n - m and (1) would hold by theorem minus_plus from Minus.v
+m - n or n - m and (1) would hold by theorem minus_add from Minus.v
 depending on whether n <= m or m <= n. However, in proving induction
 for integers constructed from natural numbers we do not need to
 require implementations of order and minus; it is enough to prove (1)
 here. *)
 
-Theorem plus_dichotomy :
+Theorem add_dichotomy :
   forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n).
 Proof.
 intros n m; induct n.
-left; exists m; apply plus_0_r.
+left; exists m; apply add_0_r.
 intros n IH.
 destruct IH as [[p H] | [p H]].
 destruct (zero_or_succ p) as [H1 | [p' H1]]; rewrite H1 in H.
-rewrite plus_0_l in H. right; exists (S 0); rewrite H; rewrite plus_succ_l; now rewrite plus_0_l.
-left; exists p'; rewrite plus_succ_r; now rewrite plus_succ_l in H.
-right; exists (S p). rewrite plus_succ_l; now rewrite H.
+rewrite add_0_l in H. right; exists (S 0); rewrite H; rewrite add_succ_l; now rewrite add_0_l.
+left; exists p'; rewrite add_succ_r; now rewrite add_succ_l in H.
+right; exists (S p). rewrite add_succ_l; now rewrite H.
 Qed.
 
 End NPlusPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NPlusOrder.v
index 8a8addefc..07eeffdfd 100644
--- a/theories/Numbers/Natural/Abstract/NPlusOrder.v
+++ b/theories/Numbers/Natural/Abstract/NPlusOrder.v
@@ -16,99 +16,99 @@ Module NPlusOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NOrderPropMod := NOrderPropFunct NAxiomsMod.
 Open Local Scope NatScope.
 
-Theorem plus_lt_mono_l : forall n m p : N, n < m <-> p + n < p + m.
-Proof NZplus_lt_mono_l.
+Theorem add_lt_mono_l : forall n m p : N, n < m <-> p + n < p + m.
+Proof NZadd_lt_mono_l.
 
-Theorem plus_lt_mono_r : forall n m p : N, n < m <-> n + p < m + p.
-Proof NZplus_lt_mono_r.
+Theorem add_lt_mono_r : forall n m p : N, n < m <-> n + p < m + p.
+Proof NZadd_lt_mono_r.
 
-Theorem plus_lt_mono : forall n m p q : N, n < m -> p < q -> n + p < m + q.
-Proof NZplus_lt_mono.
+Theorem add_lt_mono : forall n m p q : N, n < m -> p < q -> n + p < m + q.
+Proof NZadd_lt_mono.
 
-Theorem plus_le_mono_l : forall n m p : N, n <= m <-> p + n <= p + m.
-Proof NZplus_le_mono_l.
+Theorem add_le_mono_l : forall n m p : N, n <= m <-> p + n <= p + m.
+Proof NZadd_le_mono_l.
 
-Theorem plus_le_mono_r : forall n m p : N, n <= m <-> n + p <= m + p.
-Proof NZplus_le_mono_r.
+Theorem add_le_mono_r : forall n m p : N, n <= m <-> n + p <= m + p.
+Proof NZadd_le_mono_r.
 
-Theorem plus_le_mono : forall n m p q : N, n <= m -> p <= q -> n + p <= m + q.
-Proof NZplus_le_mono.
+Theorem add_le_mono : forall n m p q : N, n <= m -> p <= q -> n + p <= m + q.
+Proof NZadd_le_mono.
 
-Theorem plus_lt_le_mono : forall n m p q : N, n < m -> p <= q -> n + p < m + q.
-Proof NZplus_lt_le_mono.
+Theorem add_lt_le_mono : forall n m p q : N, n < m -> p <= q -> n + p < m + q.
+Proof NZadd_lt_le_mono.
 
-Theorem plus_le_lt_mono : forall n m p q : N, n <= m -> p < q -> n + p < m + q.
-Proof NZplus_le_lt_mono.
+Theorem add_le_lt_mono : forall n m p q : N, n <= m -> p < q -> n + p < m + q.
+Proof NZadd_le_lt_mono.
 
-Theorem plus_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n + m.
-Proof NZplus_pos_pos.
+Theorem add_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n + m.
+Proof NZadd_pos_pos.
 
-Theorem lt_plus_pos_l : forall n m : N, 0 < n -> m < n + m.
-Proof NZlt_plus_pos_l.
+Theorem lt_add_pos_l : forall n m : N, 0 < n -> m < n + m.
+Proof NZlt_add_pos_l.
 
-Theorem lt_plus_pos_r : forall n m : N, 0 < n -> m < m + n.
-Proof NZlt_plus_pos_r.
+Theorem lt_add_pos_r : forall n m : N, 0 < n -> m < m + n.
+Proof NZlt_add_pos_r.
 
-Theorem le_lt_plus_lt : forall n m p q : N, n <= m -> p + m < q + n -> p < q.
-Proof NZle_lt_plus_lt.
+Theorem le_lt_add_lt : forall n m p q : N, n <= m -> p + m < q + n -> p < q.
+Proof NZle_lt_add_lt.
 
-Theorem lt_le_plus_lt : forall n m p q : N, n < m -> p + m <= q + n -> p < q.
-Proof NZlt_le_plus_lt.
+Theorem lt_le_add_lt : forall n m p q : N, n < m -> p + m <= q + n -> p < q.
+Proof NZlt_le_add_lt.
 
-Theorem le_le_plus_le : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q.
-Proof NZle_le_plus_le.
+Theorem le_le_add_le : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q.
+Proof NZle_le_add_le.
 
-Theorem plus_lt_cases : forall n m p q : N, n + m < p + q -> n < p \/ m < q.
-Proof NZplus_lt_cases.
+Theorem add_lt_cases : forall n m p q : N, n + m < p + q -> n < p \/ m < q.
+Proof NZadd_lt_cases.
 
-Theorem plus_le_cases : forall n m p q : N, n + m <= p + q -> n <= p \/ m <= q.
-Proof NZplus_le_cases.
+Theorem add_le_cases : forall n m p q : N, n + m <= p + q -> n <= p \/ m <= q.
+Proof NZadd_le_cases.
 
-Theorem plus_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m.
-Proof NZplus_pos_cases.
+Theorem add_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m.
+Proof NZadd_pos_cases.
 
 (* Theorems true for natural numbers *)
 
-Theorem le_plus_r : forall n m : N, n <= n + m.
+Theorem le_add_r : forall n m : N, n <= n + m.
 Proof.
 intro n; induct m.
-rewrite plus_0_r; now apply eq_le_incl.
-intros m IH. rewrite plus_succ_r; now apply le_le_succ_r.
+rewrite add_0_r; now apply eq_le_incl.
+intros m IH. rewrite add_succ_r; now apply le_le_succ_r.
 Qed.
 
-Theorem lt_lt_plus_r : forall n m p : N, n < m -> n < m + p.
+Theorem lt_lt_add_r : forall n m p : N, n < m -> n < m + p.
 Proof.
-intros n m p H; rewrite <- (plus_0_r n).
-apply plus_lt_le_mono; [assumption | apply le_0_l].
+intros n m p H; rewrite <- (add_0_r n).
+apply add_lt_le_mono; [assumption | apply le_0_l].
 Qed.
 
-Theorem lt_lt_plus_l : forall n m p : N, n < m -> n < p + m.
+Theorem lt_lt_add_l : forall n m p : N, n < m -> n < p + m.
 Proof.
-intros n m p; rewrite plus_comm; apply lt_lt_plus_r.
+intros n m p; rewrite add_comm; apply lt_lt_add_r.
 Qed.
 
-Theorem plus_pos_l : forall n m : N, 0 < n -> 0 < n + m.
+Theorem add_pos_l : forall n m : N, 0 < n -> 0 < n + m.
 Proof.
-intros; apply NZplus_pos_nonneg. assumption. apply le_0_l.
+intros; apply NZadd_pos_nonneg. assumption. apply le_0_l.
 Qed.
 
-Theorem plus_pos_r : forall n m : N, 0 < m -> 0 < n + m.
+Theorem add_pos_r : forall n m : N, 0 < m -> 0 < n + m.
 Proof.
-intros; apply NZplus_nonneg_pos. apply le_0_l. assumption.
+intros; apply NZadd_nonneg_pos. apply le_0_l. assumption.
 Qed.
 
 (* The following property is used to prove the correctness of the
 definition of order on integers constructed from pairs of natural numbers *)
 
-Theorem plus_lt_repl_pair : forall n m n' m' u v : N,
+Theorem add_lt_repl_pair : forall n m n' m' u v : N,
   n + u < m + v -> n + m' == n' + m -> n' + u < m' + v.
 Proof.
 intros n m n' m' u v H1 H2.
 symmetry in H2. assert (H3 : n' + m <= n + m') by now apply eq_le_incl.
-pose proof (plus_lt_le_mono _ _ _ _ H1 H3) as H4.
-rewrite (plus_shuffle2 n u), (plus_shuffle1 m v), (plus_comm m n) in H4.
-do 2 rewrite <- plus_assoc in H4. do 2 apply <- plus_lt_mono_l in H4.
-now rewrite (plus_comm n' u), (plus_comm m' v).
+pose proof (add_lt_le_mono _ _ _ _ H1 H3) as H4.
+rewrite (add_shuffle2 n u), (add_shuffle1 m v), (add_comm m n) in H4.
+do 2 rewrite <- add_assoc in H4. do 2 apply <- add_lt_mono_l in H4.
+now rewrite (add_comm n' u), (add_comm m' v).
 Qed.
 
 End NPlusOrderPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v
index 8c0132dd9..3b1ffa79e 100644
--- a/theories/Numbers/Natural/Abstract/NTimes.v
+++ b/theories/Numbers/Natural/Abstract/NTimes.v
@@ -16,41 +16,41 @@ Module NTimesPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NPlusPropMod := NPlusPropFunct NAxiomsMod.
 Open Local Scope NatScope.
 
-Theorem times_wd :
+Theorem mul_wd :
   forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 * m1 == n2 * m2.
-Proof NZtimes_wd.
+Proof NZmul_wd.
 
-Theorem times_0_l : forall n : N, 0 * n == 0.
-Proof NZtimes_0_l.
+Theorem mul_0_l : forall n : N, 0 * n == 0.
+Proof NZmul_0_l.
 
-Theorem times_succ_l : forall n m : N, (S n) * m == n * m + m.
-Proof NZtimes_succ_l.
+Theorem mul_succ_l : forall n m : N, (S n) * m == n * m + m.
+Proof NZmul_succ_l.
 
 (** Theorems that are valid for both natural numbers and integers *)
 
-Theorem times_0_r : forall n, n * 0 == 0.
-Proof NZtimes_0_r.
+Theorem mul_0_r : forall n, n * 0 == 0.
+Proof NZmul_0_r.
 
-Theorem times_succ_r : forall n m, n * (S m) == n * m + n.
-Proof NZtimes_succ_r.
+Theorem mul_succ_r : forall n m, n * (S m) == n * m + n.
+Proof NZmul_succ_r.
 
-Theorem times_comm : forall n m : N, n * m == m * n.
-Proof NZtimes_comm.
+Theorem mul_comm : forall n m : N, n * m == m * n.
+Proof NZmul_comm.
 
-Theorem times_plus_distr_r : forall n m p : N, (n + m) * p == n * p + m * p.
-Proof NZtimes_plus_distr_r.
+Theorem mul_add_distr_r : forall n m p : N, (n + m) * p == n * p + m * p.
+Proof NZmul_add_distr_r.
 
-Theorem times_plus_distr_l : forall n m p : N, n * (m + p) == n * m + n * p.
-Proof NZtimes_plus_distr_l.
+Theorem mul_add_distr_l : forall n m p : N, n * (m + p) == n * m + n * p.
+Proof NZmul_add_distr_l.
 
-Theorem times_assoc : forall n m p : N, n * (m * p) == (n * m) * p.
-Proof NZtimes_assoc.
+Theorem mul_assoc : forall n m p : N, n * (m * p) == (n * m) * p.
+Proof NZmul_assoc.
 
-Theorem times_1_l : forall n : N, 1 * n == n.
-Proof NZtimes_1_l.
+Theorem mul_1_l : forall n : N, 1 * n == n.
+Proof NZmul_1_l.
 
-Theorem times_1_r : forall n : N, n * 1 == n.
-Proof NZtimes_1_r.
+Theorem mul_1_r : forall n : N, n * 1 == n.
+Proof NZmul_1_r.
 
 (* Theorems that cannot be proved in NZTimes *)
 
@@ -66,21 +66,21 @@ integers, the formula above could be proved by moving a * m to the left,
 factoring out a and replacing n - m by n' - m'. However, the formula is
 required in the process of constructing integers, so it has to be proved
 for natural numbers, where terms cannot be moved from one side of an
-equation to the other. The proof uses the cancellation laws plus_cancel_l
-and plus_cancel_r. *)
+equation to the other. The proof uses the cancellation laws add_cancel_l
+and add_cancel_r. *)
 
-Theorem plus_times_repl_pair : forall a n m n' m' u v : N,
+Theorem add_mul_repl_pair : forall a n m n' m' u v : N,
   a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u == a * m' + v.
 Proof.
 intros a n m n' m' u v H1 H2.
-apply (@NZtimes_wd a a) in H2; [| reflexivity].
-do 2 rewrite times_plus_distr_l in H2. symmetry in H2.
-pose proof (NZplus_wd _ _ H1 _ _ H2) as H3.
-rewrite (plus_shuffle1 (a * m)), (plus_comm (a * m) (a * n)) in H3.
-do 2 rewrite <- plus_assoc in H3. apply -> plus_cancel_l in H3.
-rewrite (plus_assoc u), (plus_comm (a * m)) in H3.
-apply -> plus_cancel_r in H3.
-now rewrite (plus_comm (a * n') u), (plus_comm (a * m') v).
+apply (@NZmul_wd a a) in H2; [| reflexivity].
+do 2 rewrite mul_add_distr_l in H2. symmetry in H2.
+pose proof (NZadd_wd _ _ H1 _ _ H2) as H3.
+rewrite (add_shuffle1 (a * m)), (add_comm (a * m) (a * n)) in H3.
+do 2 rewrite <- add_assoc in H3. apply -> add_cancel_l in H3.
+rewrite (add_assoc u), (add_comm (a * m)) in H3.
+apply -> add_cancel_r in H3.
+now rewrite (add_comm (a * n') u), (add_comm (a * m') v).
 Qed.
 
 End NTimesPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v
index 15d99c757..31f417733 100644
--- a/theories/Numbers/Natural/Abstract/NTimesOrder.v
+++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v
@@ -16,54 +16,54 @@ Module NTimesOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NPlusOrderPropMod := NPlusOrderPropFunct NAxiomsMod.
 Open Local Scope NatScope.
 
-Theorem times_lt_pred :
+Theorem mul_lt_pred :
   forall p q n m : N, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
-Proof NZtimes_lt_pred.
+Proof NZmul_lt_pred.
 
-Theorem times_lt_mono_pos_l : forall p n m : N, 0 < p -> (n < m <-> p * n < p * m).
-Proof NZtimes_lt_mono_pos_l.
+Theorem mul_lt_mono_pos_l : forall p n m : N, 0 < p -> (n < m <-> p * n < p * m).
+Proof NZmul_lt_mono_pos_l.
 
-Theorem times_lt_mono_pos_r : forall p n m : N, 0 < p -> (n < m <-> n * p < m * p).
-Proof NZtimes_lt_mono_pos_r.
+Theorem mul_lt_mono_pos_r : forall p n m : N, 0 < p -> (n < m <-> n * p < m * p).
+Proof NZmul_lt_mono_pos_r.
 
-Theorem times_cancel_l : forall n m p : N, p ~= 0 -> (p * n == p * m <-> n == m).
-Proof NZtimes_cancel_l.
+Theorem mul_cancel_l : forall n m p : N, p ~= 0 -> (p * n == p * m <-> n == m).
+Proof NZmul_cancel_l.
 
-Theorem times_cancel_r : forall n m p : N, p ~= 0 -> (n * p == m * p <-> n == m).
-Proof NZtimes_cancel_r.
+Theorem mul_cancel_r : forall n m p : N, p ~= 0 -> (n * p == m * p <-> n == m).
+Proof NZmul_cancel_r.
 
-Theorem times_id_l : forall n m : N, m ~= 0 -> (n * m == m <-> n == 1).
-Proof NZtimes_id_l.
+Theorem mul_id_l : forall n m : N, m ~= 0 -> (n * m == m <-> n == 1).
+Proof NZmul_id_l.
 
-Theorem times_id_r : forall n m : N, n ~= 0 -> (n * m == n <-> m == 1).
-Proof NZtimes_id_r.
+Theorem mul_id_r : forall n m : N, n ~= 0 -> (n * m == n <-> m == 1).
+Proof NZmul_id_r.
 
-Theorem times_le_mono_pos_l : forall n m p : N, 0 < p -> (n <= m <-> p * n <= p * m).
-Proof NZtimes_le_mono_pos_l.
+Theorem mul_le_mono_pos_l : forall n m p : N, 0 < p -> (n <= m <-> p * n <= p * m).
+Proof NZmul_le_mono_pos_l.
 
-Theorem times_le_mono_pos_r : forall n m p : N, 0 < p -> (n <= m <-> n * p <= m * p).
-Proof NZtimes_le_mono_pos_r.
+Theorem mul_le_mono_pos_r : forall n m p : N, 0 < p -> (n <= m <-> n * p <= m * p).
+Proof NZmul_le_mono_pos_r.
 
-Theorem times_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m.
-Proof NZtimes_pos_pos.
+Theorem mul_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m.
+Proof NZmul_pos_pos.
 
-Theorem lt_1_times_pos : forall n m : N, 1 < n -> 0 < m -> 1 < n * m.
-Proof NZlt_1_times_pos.
+Theorem lt_1_mul_pos : forall n m : N, 1 < n -> 0 < m -> 1 < n * m.
+Proof NZlt_1_mul_pos.
 
-Theorem eq_times_0 : forall n m : N, n * m == 0 <-> n == 0 \/ m == 0.
-Proof NZeq_times_0.
+Theorem eq_mul_0 : forall n m : N, n * m == 0 <-> n == 0 \/ m == 0.
+Proof NZeq_mul_0.
 
-Theorem neq_times_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
-Proof NZneq_times_0.
+Theorem neq_mul_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
+Proof NZneq_mul_0.
 
 Theorem eq_square_0 : forall n : N, n * n == 0 <-> n == 0.
 Proof NZeq_square_0.
 
-Theorem eq_times_0_l : forall n m : N, n * m == 0 -> m ~= 0 -> n == 0.
-Proof NZeq_times_0_l.
+Theorem eq_mul_0_l : forall n m : N, n * m == 0 -> m ~= 0 -> n == 0.
+Proof NZeq_mul_0_l.
 
-Theorem eq_times_0_r : forall n m : N, n * m == 0 -> n ~= 0 -> m == 0.
-Proof NZeq_times_0_r.
+Theorem eq_mul_0_r : forall n m : N, n * m == 0 -> n ~= 0 -> m == 0.
+Proof NZeq_mul_0_r.
 
 Theorem square_lt_mono : forall n m : N, n < m <-> n * n < m * m.
 Proof.
@@ -79,50 +79,50 @@ intros n m; split; intro;
 try assumption; apply le_0_l.
 Qed.
 
-Theorem times_2_mono_l : forall n m : N, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
-Proof NZtimes_2_mono_l.
+Theorem mul_2_mono_l : forall n m : N, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
+Proof NZmul_2_mono_l.
 
 (* Theorems that are either not valid on Z or have different proofs on N and Z *)
 
-Theorem times_le_mono_l : forall n m p : N, n <= m -> p * n <= p * m.
+Theorem mul_le_mono_l : forall n m p : N, n <= m -> p * n <= p * m.
 Proof.
-intros; apply NZtimes_le_mono_nonneg_l. apply le_0_l. assumption.
+intros; apply NZmul_le_mono_nonneg_l. apply le_0_l. assumption.
 Qed.
 
-Theorem times_le_mono_r : forall n m p : N, n <= m -> n * p <= m * p.
+Theorem mul_le_mono_r : forall n m p : N, n <= m -> n * p <= m * p.
 Proof.
-intros; apply NZtimes_le_mono_nonneg_r. apply le_0_l. assumption.
+intros; apply NZmul_le_mono_nonneg_r. apply le_0_l. assumption.
 Qed.
 
-Theorem times_lt_mono : forall n m p q : N, n < m -> p < q -> n * p < m * q.
+Theorem mul_lt_mono : forall n m p q : N, n < m -> p < q -> n * p < m * q.
 Proof.
-intros; apply NZtimes_lt_mono_nonneg; try assumption; apply le_0_l.
+intros; apply NZmul_lt_mono_nonneg; try assumption; apply le_0_l.
 Qed.
 
-Theorem times_le_mono : forall n m p q : N, n <= m -> p <= q -> n * p <= m * q.
+Theorem mul_le_mono : forall n m p q : N, n <= m -> p <= q -> n * p <= m * q.
 Proof.
-intros; apply NZtimes_le_mono_nonneg; try assumption; apply le_0_l.
+intros; apply NZmul_le_mono_nonneg; try assumption; apply le_0_l.
 Qed.
 
-Theorem lt_0_times : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0.
+Theorem lt_0_mul : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0.
 Proof.
 intros n m; split; [intro H | intros [H1 H2]].
-apply -> NZlt_0_times in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r.
-now apply NZtimes_pos_pos.
+apply -> NZlt_0_mul in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r.
+now apply NZmul_pos_pos.
 Qed.
 
-Notation times_pos := lt_0_times (only parsing).
+Notation mul_pos := lt_0_mul (only parsing).
 
-Theorem eq_times_1 : forall n m : N, n * m == 1 <-> n == 1 /\ m == 1.
+Theorem eq_mul_1 : forall n m : N, n * m == 1 <-> n == 1 /\ m == 1.
 Proof.
 intros n m.
-split; [| intros [H1 H2]; now rewrite H1, H2, times_1_l].
+split; [| intros [H1 H2]; now rewrite H1, H2, mul_1_l].
 intro H; destruct (NZlt_trichotomy n 1) as [H1 | [H1 | H1]].
-apply -> lt_1_r in H1. rewrite H1, times_0_l in H. false_hyp H neq_0_succ.
-rewrite H1, times_1_l in H; now split.
+apply -> lt_1_r in H1. rewrite H1, mul_0_l in H. false_hyp H neq_0_succ.
+rewrite H1, mul_1_l in H; now split.
 destruct (eq_0_gt_0_cases m) as [H2 | H2].
-rewrite H2, times_0_r in H; false_hyp H neq_0_succ.
-apply -> (times_lt_mono_pos_r m) in H1; [| assumption]. rewrite times_1_l in H1.
+rewrite H2, mul_0_r in H; false_hyp H neq_0_succ.
+apply -> (mul_lt_mono_pos_r m) in H1; [| assumption]. rewrite mul_1_l in H1.
 assert (H3 : 1 < n * m) by now apply (lt_1_l 0 m).
 rewrite H in H3; false_hyp H3 lt_irrefl.
 Qed.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 881b7984c..330a97ab5 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -66,14 +66,14 @@ Lemma BigNring :
  semi_ring_theory BigN.zero BigN.one BigN.add BigN.mul BigN.eq.
 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 BigNr : BigNring.
diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v
index 170dfa42f..268879aa4 100644
--- a/theories/Numbers/Natural/Binary/NBinDefs.v
+++ b/theories/Numbers/Natural/Binary/NBinDefs.v
@@ -27,9 +27,9 @@ Definition NZeq := @eq N.
 Definition NZ0 := N0.
 Definition NZsucc := Nsucc.
 Definition NZpred := Npred.
-Definition NZplus := Nplus.
+Definition NZadd := Nplus.
 Definition NZminus := Nminus.
-Definition NZtimes := Nmult.
+Definition NZmul := Nmult.
 
 Theorem NZeq_equiv : equiv N NZeq.
 Proof (eq_equiv N).
@@ -50,7 +50,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.
@@ -60,7 +60,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,16 +79,16 @@ case_eq (Psucc p); try (intros q H; rewrite <- H; now rewrite Ppred_succ).
 intro H; false_hyp H Psucc_not_one.
 Qed.
 
-Theorem NZplus_0_l : forall n : NZ, N0 + n = n.
+Theorem NZadd_0_l : forall n : NZ, N0 + n = n.
 Proof.
 reflexivity.
 Qed.
 
-Theorem NZplus_succ_l : forall n m : NZ, (NZsucc n) + m = NZsucc (n + m).
+Theorem NZadd_succ_l : forall n m : NZ, (NZsucc n) + m = NZsucc (n + m).
 Proof.
 destruct n; destruct m.
 simpl in |- *; reflexivity.
-unfold NZsucc, NZplus, Nsucc, Nplus. rewrite <- Pplus_one_succ_l; reflexivity.
+unfold NZsucc, NZadd, Nsucc, Nplus. rewrite <- Pplus_one_succ_l; reflexivity.
 simpl in |- *; reflexivity.
 simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity.
 Qed.
@@ -106,12 +106,12 @@ simpl. rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec.
 now destruct (Pminus_mask p q) as [| r |]; [| destruct r |].
 Qed.
 
-Theorem NZtimes_0_l : forall n : NZ, N0 * n = N0.
+Theorem NZmul_0_l : forall n : NZ, N0 * n = N0.
 Proof.
 destruct n; reflexivity.
 Qed.
 
-Theorem NZtimes_succ_l : forall n m : NZ, (NZsucc n) * m = n * m + m.
+Theorem NZmul_succ_l : forall n m : NZ, (NZsucc n) * m = n * m + m.
 Proof.
 destruct n as [| n]; destruct m as [| m]; simpl; try reflexivity.
 now rewrite Pmult_Sn_m, Pplus_comm.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 64f597af0..0b3586888 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -24,9 +24,9 @@ Definition NZeq := (@eq nat).
 Definition NZ0 := 0.
 Definition NZsucc := S.
 Definition NZpred := pred.
-Definition NZplus := plus.
+Definition NZadd := plus.
 Definition NZminus := minus.
-Definition NZtimes := mult.
+Definition NZmul := mult.
 
 Theorem NZeq_equiv : equiv nat NZeq.
 Proof (eq_equiv nat).
@@ -51,7 +51,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.
@@ -61,7 +61,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.
@@ -78,12 +78,12 @@ Proof.
 reflexivity.
 Qed.
 
-Theorem NZplus_0_l : forall n : nat, 0 + n = n.
+Theorem NZadd_0_l : forall n : nat, 0 + n = n.
 Proof.
 reflexivity.
 Qed.
 
-Theorem NZplus_succ_l : forall n m : nat, (S n) + m = S (n + m).
+Theorem NZadd_succ_l : forall n m : nat, (S n) + m = S (n + m).
 Proof.
 reflexivity.
 Qed.
@@ -98,12 +98,12 @@ Proof.
 intros n m; induction n m using nat_double_ind; simpl; auto. apply NZminus_0_r.
 Qed.
 
-Theorem NZtimes_0_l : forall n : nat, 0 * n = 0.
+Theorem NZmul_0_l : forall n : nat, 0 * n = 0.
 Proof.
 reflexivity.
 Qed.
 
-Theorem NZtimes_succ_l : forall n m : nat, S n * m = n * m + m.
+Theorem NZmul_succ_l : forall n m : nat, S n * m = n * m + m.
 Proof.
 intros n m; now rewrite plus_comm.
 Qed.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 115f78be0..54d7aec52 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -35,9 +35,9 @@ Definition NZeq := N.eq.
 Definition NZ0 := N.zero.
 Definition NZsucc := N.succ.
 Definition NZpred := N.pred.
-Definition NZplus := N.add.
+Definition NZadd := N.add.
 Definition NZminus := N.sub.
-Definition NZtimes := N.mul.
+Definition NZmul := N.mul.
 
 Theorem NZeq_equiv : equiv N.t N.eq.
 Proof.
@@ -64,7 +64,7 @@ rewrite 2 N.spec_pred0; congruence.
 rewrite 2 N.spec_pred; f_equal; auto; try omega.
 Qed.
 
-Add Morphism NZplus with signature N.eq ==> N.eq ==> N.eq as NZplus_wd.
+Add Morphism NZadd with signature N.eq ==> N.eq ==> N.eq as NZadd_wd.
 Proof.
 unfold N.eq; intros; rewrite 2 N.spec_add; f_equal; auto.
 Qed.
@@ -77,7 +77,7 @@ rewrite 2 N.spec_sub0; f_equal; congruence.
 rewrite 2 N.spec_sub; f_equal; congruence.
 Qed.
 
-Add Morphism NZtimes with signature N.eq ==> N.eq ==> N.eq as NZtimes_wd.
+Add Morphism NZmul with signature N.eq ==> N.eq ==> N.eq as NZmul_wd.
 Proof.
 unfold N.eq; intros; rewrite 2 N.spec_mul; f_equal; auto.
 Qed.
@@ -137,12 +137,12 @@ Qed.
 
 End Induction.
 
-Theorem NZplus_0_l : forall n, 0 + n == n.
+Theorem NZadd_0_l : forall n, 0 + n == n.
 Proof.
 intros; red; rewrite N.spec_add, N.spec_0; auto with zarith.
 Qed.
 
-Theorem NZplus_succ_l : forall n m, (N.succ n) + m == N.succ (n + m).
+Theorem NZadd_succ_l : forall n m, (N.succ n) + m == N.succ (n + m).
 Proof.
 intros; red; rewrite N.spec_add, 2 N.spec_succ, N.spec_add; auto with zarith.
 Qed.
@@ -169,13 +169,13 @@ rewrite N.spec_pred, N.spec_sub; auto with zarith.
 rewrite N.spec_sub; auto with zarith.
 Qed.
 
-Theorem NZtimes_0_l : forall n, 0 * n == 0.
+Theorem NZmul_0_l : forall n, 0 * n == 0.
 Proof.
 intros; red.
 rewrite N.spec_mul, N.spec_0; auto with zarith.
 Qed.
 
-Theorem NZtimes_succ_l : forall n m, (N.succ n) * m == n * m + m.
+Theorem NZmul_succ_l : forall n m, (N.succ n) * m == n * m + m.
 Proof.
 intros; red.
 rewrite N.spec_add, 2 N.spec_mul, N.spec_succ; ring.