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

5 files changed, 215 insertions, 215 deletions

diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index ef19069955..516cf5b42b 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 673b819ba4..6fb72ed4a9 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 45148bc20c..00d178c0d9 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 7503ddce22..9f93e0a1bf 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 b48acc598d..ebb2a9b5d0 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.