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

8 files changed, 263 insertions, 263 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index a4e8c056fe..c31f216a30 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 e90977e3d7..eb46e69de0 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 369c1261cf..57d33e7b63 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 0c24ca9849..81b41dc03b 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 71122e3a5a..67443acff2 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 8a8addefc7..07eeffdfd8 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 8c0132dd99..3b1ffa79e8 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 15d99c7575..31f4177335 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.