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

for increased consistency with bignums parts 

(commit part II: names of files + additional translation minus --> sub)



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

14 files changed, 225 insertions, 225 deletions

diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NAdd.v
index 67443acff..37244159f 100644
--- a/theories/Numbers/Natural/Abstract/NPlus.v
+++ b/theories/Numbers/Natural/Abstract/NAdd.v
@@ -12,7 +12,7 @@
 
 Require Export NBase.
 
-Module NPlusPropFunct (Import NAxiomsMod : NAxiomsSig).
+Module NAddPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NBasePropMod := NBasePropFunct NAxiomsMod.
 
 Open Local Scope NatScope.
@@ -64,7 +64,7 @@ Proof NZadd_cancel_r.
 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 add_0_l from NPlusSig *)
+(* The next command does not work with the axiom add_0_l from NAddSig *)
 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
@@ -133,10 +133,10 @@ 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_add from Minus.v
+m - n or n - m and (1) would hold by theorem sub_add from Sub.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)
+require implementations of order and sub; it is enough to prove (1)
 here. *)
 
 Theorem add_dichotomy :
@@ -152,5 +152,5 @@ 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.
+End NAddPropFunct.
 
diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v
index 07eeffdfd..59f1c9347 100644
--- a/theories/Numbers/Natural/Abstract/NPlusOrder.v
+++ b/theories/Numbers/Natural/Abstract/NAddOrder.v
@@ -12,7 +12,7 @@
 
 Require Export NOrder.
 
-Module NPlusOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
+Module NAddOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NOrderPropMod := NOrderPropFunct NAxiomsMod.
 Open Local Scope NatScope.
 
@@ -111,4 +111,4 @@ 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.
+End NAddOrderPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index c31f216a3..60f2aae7d 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -26,7 +26,7 @@ Notation S := NZsucc.
 Notation P := NZpred.
 Notation add := NZadd.
 Notation mul := NZmul.
-Notation minus := NZminus.
+Notation sub := NZsub.
 Notation lt := NZlt.
 Notation le := NZle.
 Notation min := NZmin.
@@ -36,7 +36,7 @@ Notation "x ~= y" := (~ Neq x y) (at level 70) : NatScope.
 Notation "0" := NZ0 : NatScope.
 Notation "1" := (NZsucc NZ0) : NatScope.
 Notation "x + y" := (NZadd x y) : NatScope.
-Notation "x - y" := (NZminus x y) : NatScope.
+Notation "x - y" := (NZsub x y) : NatScope.
 Notation "x * y" := (NZmul x y) : NatScope.
 Notation "x < y" := (NZlt x y) : NatScope.
 Notation "x <= y" := (NZle x y) : NatScope.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index eb46e69de..0d7bc63eb 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -12,7 +12,7 @@
 
 Require Export Decidable.
 Require Export NAxioms.
-Require Import NZTimesOrder. (* The last property functor on NZ, which subsumes all others *)
+Require Import NZMulOrder. (* The last property functor on NZ, which subsumes all others *)
 
 Module NBasePropFunct (Import NAxiomsMod : NAxiomsSig).
 
@@ -22,16 +22,16 @@ Open Local Scope NatScope.
 ones, to get all properties of NZ at once. This way we will include them
 only one time. *)
 
-Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod.
+Module Export NZMulOrderMod := NZMulOrderPropFunct NZOrdAxiomsMod.
 
 (* Here we probably need to re-prove all axioms declared in NAxioms.v to
 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
+this way, one only has to consult, for example, NAdd.v to see all
 available properties for add, i.e., one does not have to go to NAxioms.v
-for axioms and NZPlus.v for theorems. *)
+for axioms and NZAdd.v for theorems. *)
 
 Theorem succ_wd : forall n1 n2 : N, n1 == n2 -> S n1 == S n2.
 Proof NZsucc_wd.
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
deleted file mode 100644
index 81b41dc03..000000000
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ /dev/null
@@ -1,180 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-(*                      Evgeny Makarov, INRIA, 2007                     *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-Require Export NTimesOrder.
-
-Module NMinusPropFunct (Import NAxiomsMod : NAxiomsSig).
-Module Export NTimesOrderPropMod := NTimesOrderPropFunct NAxiomsMod.
-Open Local Scope NatScope.
-
-Theorem minus_wd :
-  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 - m1 == n2 - m2.
-Proof NZminus_wd.
-
-Theorem minus_0_r : forall n : N, n - 0 == n.
-Proof NZminus_0_r.
-
-Theorem minus_succ_r : forall n m : N, n - (S m) == P (n - m).
-Proof NZminus_succ_r.
-
-Theorem minus_1_r : forall n : N, n - 1 == P n.
-Proof.
-intro n; rewrite minus_succ_r; now rewrite minus_0_r.
-Qed.
-
-Theorem minus_0_l : forall n : N, 0 - n == 0.
-Proof.
-induct n.
-apply minus_0_r.
-intros n IH; rewrite minus_succ_r; rewrite IH. now apply pred_0.
-Qed.
-
-Theorem minus_succ : forall n m : N, S n - S m == n - m.
-Proof.
-intro n; induct m.
-rewrite minus_succ_r. do 2 rewrite minus_0_r. now rewrite pred_succ.
-intros m IH. rewrite minus_succ_r. rewrite IH. now rewrite minus_succ_r.
-Qed.
-
-Theorem minus_diag : forall n : N, n - n == 0.
-Proof.
-induct n. apply minus_0_r. intros n IH; rewrite minus_succ; now rewrite IH.
-Qed.
-
-Theorem minus_gt : forall n m : N, n > m -> n - m ~= 0.
-Proof.
-intros n m H; elim H using lt_ind_rel; clear n m H.
-solve_relation_wd.
-intro; rewrite minus_0_r; apply neq_succ_0.
-intros; now rewrite minus_succ.
-Qed.
-
-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 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 <- (add_1_l m). rewrite <- (add_1_l (m - n)).
-symmetry; now apply add_minus_assoc.
-Qed.
-
-Theorem add_minus : forall n m : N, (n + m) - m == n.
-Proof.
-intros n m. rewrite <- add_minus_assoc by (apply le_refl).
-rewrite minus_diag; now rewrite add_0_r.
-Qed.
-
-Theorem minus_add : forall n m : N, n <= m -> (m - n) + n == m.
-Proof.
-intros n m H. rewrite add_comm. rewrite add_minus_assoc by assumption.
-rewrite add_comm. apply add_minus.
-Qed.
-
-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 add_comm in H1. now rewrite add_minus in H1.
-Qed.
-
-Theorem add_minus_eq_r : forall n m p : N, m + p == n -> n - p == m.
-Proof.
-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 add_minus_assoc and minus_0_le, which is proven below. *)
-
-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 add_0_l.
-intros n m IH H1. rewrite minus_succ in H1. apply IH in H1.
-rewrite add_succ_l; now rewrite H1.
-Qed.
-
-Theorem minus_add_distr : forall n m p : N, n - (m + p) == (n - m) - p.
-Proof.
-intros n m; induct p.
-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 add_minus_swap : forall n m p : N, p <= n -> n + m - p == n - p + m.
-Proof.
-intros n m p H.
-rewrite (add_comm n m).
-rewrite <- add_minus_assoc by assumption.
-now rewrite (add_comm m (n - p)).
-Qed.
-
-(** Minus and order *)
-
-Theorem le_minus_l : forall n m : N, n - m <= n.
-Proof.
-intro n; induct m.
-rewrite minus_0_r; now apply eq_le_incl.
-intros m IH. rewrite minus_succ_r.
-apply le_trans with (n - m); [apply le_pred_l | assumption].
-Qed.
-
-Theorem minus_0_le : forall n m : N, n - m == 0 <-> n <= m.
-Proof.
-double_induct n m.
-intro m; split; intro; [apply le_0_l | apply minus_0_l].
-intro m; rewrite minus_0_r; split; intro H;
-[false_hyp H neq_succ_0 | false_hyp H nle_succ_0].
-intros n m H. rewrite <- succ_le_mono. now rewrite minus_succ.
-Qed.
-
-(** Minus and mul *)
-
-Theorem mul_pred_r : forall n m : N, n * (P m) == n * m - n.
-Proof.
-intros n m; cases m.
-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 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, 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 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 mul_le_mono_r).
-apply mul_0_l.
-Qed.
-
-Theorem mul_minus_distr_l : forall n m p : N, p * (n - m) == p * n - p * m.
-Proof.
-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/NTimes.v b/theories/Numbers/Natural/Abstract/NMul.v
index 3b1ffa79e..69b284fdc 100644
--- a/theories/Numbers/Natural/Abstract/NTimes.v
+++ b/theories/Numbers/Natural/Abstract/NMul.v
@@ -10,10 +10,10 @@
 
 (*i $Id$ i*)
 
-Require Export NPlus.
+Require Export NAdd.
 
-Module NTimesPropFunct (Import NAxiomsMod : NAxiomsSig).
-Module Export NPlusPropMod := NPlusPropFunct NAxiomsMod.
+Module NMulPropFunct (Import NAxiomsMod : NAxiomsSig).
+Module Export NAddPropMod := NAddPropFunct NAxiomsMod.
 Open Local Scope NatScope.
 
 Theorem mul_wd :
@@ -52,7 +52,7 @@ Proof NZmul_1_l.
 Theorem mul_1_r : forall n : N, n * 1 == n.
 Proof NZmul_1_r.
 
-(* Theorems that cannot be proved in NZTimes *)
+(* Theorems that cannot be proved in NZMul *)
 
 (* In proving the correctness of the definition of multiplication on
 integers constructed from pairs of natural numbers, we'll need the
@@ -83,5 +83,5 @@ apply -> add_cancel_r in H3.
 now rewrite (add_comm (a * n') u), (add_comm (a * m') v).
 Qed.
 
-End NTimesPropFunct.
+End NMulPropFunct.
 
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v
index 31f417733..ac4cc5e9e 100644
--- a/theories/Numbers/Natural/Abstract/NTimesOrder.v
+++ b/theories/Numbers/Natural/Abstract/NMulOrder.v
@@ -10,10 +10,10 @@
 
 (*i $Id$ i*)
 
-Require Export NPlusOrder.
+Require Export NAddOrder.
 
-Module NTimesOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
-Module Export NPlusOrderPropMod := NPlusOrderPropFunct NAxiomsMod.
+Module NMulOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
+Module Export NAddOrderPropMod := NAddOrderPropFunct NAxiomsMod.
 Open Local Scope NatScope.
 
 Theorem mul_lt_pred :
@@ -127,5 +127,5 @@ assert (H3 : 1 < n * m) by now apply (lt_1_l 0 m).
 rewrite H in H3; false_hyp H3 lt_irrefl.
 Qed.
 
-End NTimesOrderPropFunct.
+End NMulOrderPropFunct.
 
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index bc5753d16..bcd4b92d6 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -10,10 +10,10 @@
 
 (*i $Id$ i*)
 
-Require Export NTimes.
+Require Export NMul.
 
 Module NOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
-Module Export NTimesPropMod := NTimesPropFunct NAxiomsMod.
+Module Export NMulPropMod := NMulPropFunct NAxiomsMod.
 Open Local Scope NatScope.
 
 (* The tactics le_less, le_equal and le_elim are inherited from NZOrder.v *)
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index 78b647d99..5303bf8e5 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -13,10 +13,10 @@
 (** This file defined the strong (course-of-value, well-founded) recursion
 and proves its properties *)
 
-Require Export NMinus.
+Require Export NSub.
 
 Module NStrongRecPropFunct (Import NAxiomsMod : NAxiomsSig).
-Module Export NMinusPropMod := NMinusPropFunct NAxiomsMod.
+Module Export NSubPropMod := NSubPropFunct NAxiomsMod.
 Open Local Scope NatScope.
 
 Section StrongRecursion.
diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v
new file mode 100644
index 000000000..cfeb6709b
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NSub.v
@@ -0,0 +1,180 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Export NMulOrder.
+
+Module NSubPropFunct (Import NAxiomsMod : NAxiomsSig).
+Module Export NMulOrderPropMod := NMulOrderPropFunct NAxiomsMod.
+Open Local Scope NatScope.
+
+Theorem sub_wd :
+  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 - m1 == n2 - m2.
+Proof NZsub_wd.
+
+Theorem sub_0_r : forall n : N, n - 0 == n.
+Proof NZsub_0_r.
+
+Theorem sub_succ_r : forall n m : N, n - (S m) == P (n - m).
+Proof NZsub_succ_r.
+
+Theorem sub_1_r : forall n : N, n - 1 == P n.
+Proof.
+intro n; rewrite sub_succ_r; now rewrite sub_0_r.
+Qed.
+
+Theorem sub_0_l : forall n : N, 0 - n == 0.
+Proof.
+induct n.
+apply sub_0_r.
+intros n IH; rewrite sub_succ_r; rewrite IH. now apply pred_0.
+Qed.
+
+Theorem sub_succ : forall n m : N, S n - S m == n - m.
+Proof.
+intro n; induct m.
+rewrite sub_succ_r. do 2 rewrite sub_0_r. now rewrite pred_succ.
+intros m IH. rewrite sub_succ_r. rewrite IH. now rewrite sub_succ_r.
+Qed.
+
+Theorem sub_diag : forall n : N, n - n == 0.
+Proof.
+induct n. apply sub_0_r. intros n IH; rewrite sub_succ; now rewrite IH.
+Qed.
+
+Theorem sub_gt : forall n m : N, n > m -> n - m ~= 0.
+Proof.
+intros n m H; elim H using lt_ind_rel; clear n m H.
+solve_relation_wd.
+intro; rewrite sub_0_r; apply neq_succ_0.
+intros; now rewrite sub_succ.
+Qed.
+
+Theorem add_sub_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 sub_0_r.
+intros p IH H. do 2 rewrite sub_succ_r.
+rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l).
+rewrite add_pred_r by (apply sub_gt; now apply -> le_succ_l).
+reflexivity.
+Qed.
+
+Theorem sub_succ_l : forall n m : N, n <= m -> S m - n == S (m - n).
+Proof.
+intros n m H. rewrite <- (add_1_l m). rewrite <- (add_1_l (m - n)).
+symmetry; now apply add_sub_assoc.
+Qed.
+
+Theorem add_sub : forall n m : N, (n + m) - m == n.
+Proof.
+intros n m. rewrite <- add_sub_assoc by (apply le_refl).
+rewrite sub_diag; now rewrite add_0_r.
+Qed.
+
+Theorem sub_add : forall n m : N, n <= m -> (m - n) + n == m.
+Proof.
+intros n m H. rewrite add_comm. rewrite add_sub_assoc by assumption.
+rewrite add_comm. apply add_sub.
+Qed.
+
+Theorem add_sub_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 add_comm in H1. now rewrite add_sub in H1.
+Qed.
+
+Theorem add_sub_eq_r : forall n m p : N, m + p == n -> n - p == m.
+Proof.
+intros n m p H; rewrite add_comm in H; now apply add_sub_eq_l.
+Qed.
+
+(* This could be proved by adding m to both sides. Then the proof would
+use add_sub_assoc and sub_0_le, which is proven below. *)
+
+Theorem add_sub_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 sub_0_l in H1. symmetry in H1; false_hyp H1 H.
+intro n; rewrite sub_0_r; now rewrite add_0_l.
+intros n m IH H1. rewrite sub_succ in H1. apply IH in H1.
+rewrite add_succ_l; now rewrite H1.
+Qed.
+
+Theorem sub_add_distr : forall n m p : N, n - (m + p) == (n - m) - p.
+Proof.
+intros n m; induct p.
+rewrite add_0_r; now rewrite sub_0_r.
+intros p IH. rewrite add_succ_r; do 2 rewrite sub_succ_r. now rewrite IH.
+Qed.
+
+Theorem add_sub_swap : forall n m p : N, p <= n -> n + m - p == n - p + m.
+Proof.
+intros n m p H.
+rewrite (add_comm n m).
+rewrite <- add_sub_assoc by assumption.
+now rewrite (add_comm m (n - p)).
+Qed.
+
+(** Sub and order *)
+
+Theorem le_sub_l : forall n m : N, n - m <= n.
+Proof.
+intro n; induct m.
+rewrite sub_0_r; now apply eq_le_incl.
+intros m IH. rewrite sub_succ_r.
+apply le_trans with (n - m); [apply le_pred_l | assumption].
+Qed.
+
+Theorem sub_0_le : forall n m : N, n - m == 0 <-> n <= m.
+Proof.
+double_induct n m.
+intro m; split; intro; [apply le_0_l | apply sub_0_l].
+intro m; rewrite sub_0_r; split; intro H;
+[false_hyp H neq_succ_0 | false_hyp H nle_succ_0].
+intros n m H. rewrite <- succ_le_mono. now rewrite sub_succ.
+Qed.
+
+(** Sub and mul *)
+
+Theorem mul_pred_r : forall n m : N, n * (P m) == n * m - n.
+Proof.
+intros n m; cases m.
+now rewrite pred_0, mul_0_r, sub_0_l.
+intro m; rewrite pred_succ, mul_succ_r, <- add_sub_assoc.
+now rewrite sub_diag, add_0_r.
+now apply eq_le_incl.
+Qed.
+
+Theorem mul_sub_distr_r : forall n m p : N, (n - m) * p == n * p - m * p.
+Proof.
+intros n m p; induct n.
+now rewrite sub_0_l, mul_0_l, sub_0_l.
+intros n IH. destruct (le_gt_cases m n) as [H | H].
+rewrite sub_succ_l by assumption. do 2 rewrite mul_succ_l.
+rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p).
+rewrite <- (add_sub_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 <- sub_0_le.
+setoid_replace ((S n * p) - m * p) with 0 by (apply <- sub_0_le; now apply mul_le_mono_r).
+apply mul_0_l.
+Qed.
+
+Theorem mul_sub_distr_l : forall n m p : N, p * (n - m) == p * n - p * m.
+Proof.
+intros n m p; rewrite (mul_comm p (n - m)), (mul_comm p n), (mul_comm p m).
+apply mul_sub_distr_r.
+Qed.
+
+End NSubPropFunct.
+
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 330a97ab5..485480fa0 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -20,14 +20,14 @@ Require Import Cyclic31.
 Require Import NSig.
 Require Import NSigNAxioms.
 Require Import NMake.
-Require Import NMinus.
+Require Import NSub.
 
 Module BigN <: NType := NMake.Make Int31Cyclic.
 
 (** Module [BigN] implements [NAxiomsSig] *)
 
 Module Export BigNAxiomsMod := NSig_NAxioms BigN.
-Module Export BigNMinusPropMod := NMinusPropFunct BigNAxiomsMod.
+Module Export BigNSubPropMod := NSubPropFunct BigNAxiomsMod.
 
 (** Notations about [BigN] *)
 
diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v
index 268879aa4..e0f3fdf4b 100644
--- a/theories/Numbers/Natural/Binary/NBinDefs.v
+++ b/theories/Numbers/Natural/Binary/NBinDefs.v
@@ -12,7 +12,7 @@
 
 Require Import BinPos.
 Require Export BinNat.
-Require Import NMinus.
+Require Import NSub.
 
 Open Local Scope N_scope.
 
@@ -28,7 +28,7 @@ Definition NZ0 := N0.
 Definition NZsucc := Nsucc.
 Definition NZpred := Npred.
 Definition NZadd := Nplus.
-Definition NZminus := Nminus.
+Definition NZsub := Nminus.
 Definition NZmul := Nmult.
 
 Theorem NZeq_equiv : equiv N NZeq.
@@ -55,7 +55,7 @@ Proof.
 congruence.
 Qed.
 
-Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd.
+Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.
 Proof.
 congruence.
 Qed.
@@ -93,12 +93,12 @@ simpl in |- *; reflexivity.
 simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity.
 Qed.
 
-Theorem NZminus_0_r : forall n : NZ, n - N0 = n.
+Theorem NZsub_0_r : forall n : NZ, n - N0 = n.
 Proof.
 now destruct n.
 Qed.
 
-Theorem NZminus_succ_r : forall n m : NZ, n - (NZsucc m) = NZpred (n - m).
+Theorem NZsub_succ_r : forall n m : NZ, n - (NZsucc m) = NZpred (n - m).
 Proof.
 destruct n as [| p]; destruct m as [| q]; try reflexivity.
 now destruct p.
@@ -242,7 +242,7 @@ Qed.
 
 End NBinaryAxiomsMod.
 
-Module Export NBinaryMinusPropMod := NMinusPropFunct NBinaryAxiomsMod.
+Module Export NBinarySubPropMod := NSubPropFunct NBinaryAxiomsMod.
 
 (* Some fun comparing the efficiency of the generic log defined
 by strong (course-of-value) recursion and the log defined by recursion
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 0b3586888..8d9e17fb0 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -13,7 +13,7 @@
 Require Import Arith.
 Require Import Min.
 Require Import Max.
-Require Import NMinus.
+Require Import NSub.
 
 Module NPeanoAxiomsMod <: NAxiomsSig.
 Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
@@ -25,7 +25,7 @@ Definition NZ0 := 0.
 Definition NZsucc := S.
 Definition NZpred := pred.
 Definition NZadd := plus.
-Definition NZminus := minus.
+Definition NZsub := minus.
 Definition NZmul := mult.
 
 Theorem NZeq_equiv : equiv nat NZeq.
@@ -56,7 +56,7 @@ Proof.
 congruence.
 Qed.
 
-Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd.
+Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.
 Proof.
 congruence.
 Qed.
@@ -88,14 +88,14 @@ Proof.
 reflexivity.
 Qed.
 
-Theorem NZminus_0_r : forall n : nat, n - 0 = n.
+Theorem NZsub_0_r : forall n : nat, n - 0 = n.
 Proof.
 intro n; now destruct n.
 Qed.
 
-Theorem NZminus_succ_r : forall n m : nat, n - (S m) = pred (n - m).
+Theorem NZsub_succ_r : forall n m : nat, n - (S m) = pred (n - m).
 Proof.
-intros n m; induction n m using nat_double_ind; simpl; auto. apply NZminus_0_r.
+intros n m; induction n m using nat_double_ind; simpl; auto. apply NZsub_0_r.
 Qed.
 
 Theorem NZmul_0_l : forall n : nat, 0 * n = 0.
@@ -216,5 +216,5 @@ End NPeanoAxiomsMod.
 
 (* Now we apply the largest property functor *)
 
-Module Export NPeanoMinusPropMod := NMinusPropFunct NPeanoAxiomsMod.
+Module Export NPeanoSubPropMod := NSubPropFunct NPeanoAxiomsMod.
 
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 54d7aec52..4f558e80a 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -36,7 +36,7 @@ Definition NZ0 := N.zero.
 Definition NZsucc := N.succ.
 Definition NZpred := N.pred.
 Definition NZadd := N.add.
-Definition NZminus := N.sub.
+Definition NZsub := N.sub.
 Definition NZmul := N.mul.
 
 Theorem NZeq_equiv : equiv N.t N.eq.
@@ -69,7 +69,7 @@ Proof.
 unfold N.eq; intros; rewrite 2 N.spec_add; f_equal; auto.
 Qed.
 
-Add Morphism NZminus with signature N.eq ==> N.eq ==> N.eq as NZminus_wd.
+Add Morphism NZsub with signature N.eq ==> N.eq ==> N.eq as NZsub_wd.
 Proof.
 unfold N.eq; intros x x' Hx y y' Hy.
 destruct (Z_lt_le_dec [x] [y]).
@@ -147,13 +147,13 @@ Proof.
 intros; red; rewrite N.spec_add, 2 N.spec_succ, N.spec_add; auto with zarith.
 Qed.
 
-Theorem NZminus_0_r : forall n, n - 0 == n.
+Theorem NZsub_0_r : forall n, n - 0 == n.
 Proof.
 intros; red; rewrite N.spec_sub; rewrite N.spec_0; auto with zarith.
 apply N.spec_pos.
 Qed.
 
-Theorem NZminus_succ_r : forall n m, n - (N.succ m) == N.pred (n - m).
+Theorem NZsub_succ_r : forall n m, n - (N.succ m) == N.pred (n - m).
 Proof.
 intros; red.
 destruct (Z_lt_le_dec [n] [N.succ m]) as [H|H].