Added transitivity and irreflexivity of <, as well as < -elimination for binary positive numbers.

Added directory contribs/micromega with the generalization of Frédéric Besson's micromega tactic for an arbitrary ordered ring. So far no tactic has been defined. One has to apply the theorems and find the certificate, which is necessary to solve inequations, manually.


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

12 files changed, 241 insertions, 356 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index ab863eb1f6..bde3d9a920 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -10,7 +10,7 @@ Open Local Scope NatIntScope.
 Notation Z := NZ (only parsing).
 Notation E := NZE (only parsing).
 
-Parameter Inline Zopp : Z -> Z.
+Parameter Zopp : Z -> Z.
 
 Add Morphism Zopp with signature E ==> E as Zopp_wd.
 
diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v
index 295f5355aa..e0ef2f15d9 100644
--- a/theories/Numbers/Integer/Abstract/ZOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZOrder.v
@@ -23,6 +23,9 @@ Proof NZlt_le_incl.
 Theorem Zlt_neq : forall n m : Z, n < m -> n ~= m.
 Proof NZlt_neq.
 
+Theorem Zlt_le_neq : forall n m : Z, n < m <-> n <= m /\ n ~= m.
+Proof NZlt_le_neq.
+
 Theorem Zle_refl : forall n : Z, n <= n.
 Proof NZle_refl.
 
diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
index bab1bb4a08..6a13aa3db6 100644
--- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
@@ -30,14 +30,32 @@ Proof NZplus_lt_le_mono.
 Theorem Zplus_le_lt_mono : forall n m p q : Z, n <= m -> p < q -> n + p < m + q.
 Proof NZplus_le_lt_mono.
 
+Theorem Zplus_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n + m.
+Proof NZplus_pos_pos.
+
+Theorem Zplus_pos_nonneg : forall n m : Z, 0 < n -> 0 <= m -> 0 < n + m.
+Proof NZplus_pos_nonneg.
+
+Theorem Zplus_nonneg_pos : forall n m : Z, 0 <= n -> 0 < m -> 0 < n + m.
+Proof NZplus_nonneg_pos.
+
+Theorem Zplus_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n + m.
+Proof NZplus_nonneg_nonneg.
+
+Theorem Zlt_plus_pos_l : forall n m : Z, 0 < n -> m < n + m.
+Proof NZlt_plus_pos_l.
+
+Theorem Zlt_plus_pos_r : forall n m : Z, 0 < n -> m < m + n.
+Proof NZlt_plus_pos_r.
+
 Theorem Zle_lt_plus_lt : forall n m p q : Z, n <= m -> p + m < q + n -> p < q.
 Proof NZle_lt_plus_lt.
 
 Theorem Zlt_le_plus_lt : forall n m p q : Z, n < m -> p + m <= q + n -> p < q.
 Proof NZlt_le_plus_lt.
 
-Theorem Zle_le_plus_lt : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q.
-Proof NZle_le_plus_lt.
+Theorem Zle_le_plus_le : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q.
+Proof NZle_le_plus_le.
 
 Theorem Zplus_lt_cases : forall n m p q : Z, n + m < p + q -> n < p \/ m < q.
 Proof NZplus_lt_cases.
@@ -57,89 +75,6 @@ Proof NZplus_nonpos_cases.
 Theorem Zplus_nonneg_cases : forall n m : Z, 0 <= n + m -> 0 <= n \/ 0 <= m.
 Proof NZplus_nonneg_cases.
 
-(** Multiplication and order *)
-
-Theorem Ztimes_lt_pred :
-  forall p q n m : Z, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
-Proof NZtimes_lt_pred.
-
-Theorem Ztimes_lt_mono_pos_l : forall p n m : Z, 0 < p -> (n < m <-> p * n < p * m).
-Proof NZtimes_lt_mono_pos_l.
-
-Theorem Ztimes_lt_mono_pos_r : forall p n m : Z, 0 < p -> (n < m <-> n * p < m * p).
-Proof NZtimes_lt_mono_pos_r.
-
-Theorem Ztimes_lt_mono_neg_l : forall p n m : Z, p < 0 -> (n < m <-> p * m < p * n).
-Proof NZtimes_lt_mono_neg_l.
-
-Theorem Ztimes_lt_mono_neg_r : forall p n m : Z, p < 0 -> (n < m <-> m * p < n * p).
-Proof NZtimes_lt_mono_neg_r.
-
-Theorem Ztimes_le_mono_nonneg_l : forall n m p : Z, 0 <= p -> n <= m -> p * n <= p * m.
-Proof NZtimes_le_mono_nonneg_l.
-
-Theorem Ztimes_le_mono_nonpos_l : forall n m p : Z, p <= 0 -> n <= m -> p * m <= p * n.
-Proof NZtimes_le_mono_nonpos_l.
-
-Theorem Ztimes_le_mono_nonneg_r : forall n m p : Z, 0 <= p -> n <= m -> n * p <= m * p.
-Proof NZtimes_le_mono_nonneg_r.
-
-Theorem Ztimes_le_mono_nonpos_r : forall n m p : Z, p <= 0 -> n <= m -> m * p <= n * p.
-Proof NZtimes_le_mono_nonpos_r.
-
-Theorem Ztimes_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m).
-Proof NZtimes_cancel_l.
-
-Theorem Ztimes_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m).
-Proof NZtimes_le_mono_pos_l.
-
-Theorem Ztimes_le_mono_pos_r : forall n m p : Z, 0 < p -> (n <= m <-> n * p <= m * p).
-Proof NZtimes_le_mono_pos_r.
-
-Theorem Ztimes_le_mono_neg_l : forall n m p : Z, p < 0 -> (n <= m <-> p * m <= p * n).
-Proof NZtimes_le_mono_neg_l.
-
-Theorem Ztimes_le_mono_neg_r : forall n m p : Z, p < 0 -> (n <= m <-> m * p <= n * p).
-Proof NZtimes_le_mono_neg_r.
-
-Theorem Ztimes_lt_mono :
-  forall n m p q : Z, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q.
-Proof NZtimes_lt_mono.
-
-Theorem Ztimes_le_mono :
-  forall n m p q : Z, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q.
-Proof NZtimes_le_mono.
-
-Theorem Ztimes_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n * m.
-Proof NZtimes_pos_pos.
-
-Theorem Ztimes_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m.
-Proof NZtimes_nonneg_nonneg.
-
-Theorem Ztimes_neg_neg : forall n m : Z, n < 0 -> m < 0 -> 0 < n * m.
-Proof NZtimes_neg_neg.
-
-Theorem Ztimes_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m.
-Proof NZtimes_nonpos_nonpos.
-
-Theorem Ztimes_pos_neg : forall n m : Z, 0 < n -> m < 0 -> n * m < 0.
-Proof NZtimes_pos_neg.
-
-Theorem Ztimes_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0.
-Proof NZtimes_nonneg_nonpos.
-
-Theorem Ztimes_neg_pos : forall n m : Z, n < 0 -> 0 < m -> n * m < 0.
-Proof NZtimes_neg_pos.
-
-Theorem Ztimes_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0.
-Proof NZtimes_nonpos_nonneg.
-
-Theorem Ztimes_eq_0 : forall n m : Z, n * m == 0 -> n == 0 \/ m == 0.
-Proof NZtimes_eq_0.
-
-Theorem Ztimes_neq_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
-Proof NZtimes_neq_0.
-
 (** Theorems that are either not valid on N or have different proofs on N and Z *)
 
 (** Minus and order *)
@@ -252,7 +187,7 @@ Qed.
 
 Theorem Zle_le_minus_lt : forall n m p q : Z, n <= m -> p - n <= q - m -> p <= q.
 Proof.
-intros n m p q H1 H2. apply (Zle_le_plus_lt (- m) (- n));
+intros n m p q H1 H2. apply (Zle_le_plus_le (- m) (- n));
 [now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_minus].
 Qed.
 
diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
index d63dc0d8c6..4381420950 100644
--- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
@@ -94,6 +94,9 @@ Theorem Ztimes_neg :
   forall n m : Z, n * m < 0 <-> (n < 0 /\ m > 0) \/ (n > 0 /\ m < 0).
 Proof NZtimes_neg.
 
+Theorem Ztimes_2_mono_l : forall n m : Z, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
+Proof NZtimes_2_mono_l.
+
 (** Theorems that are either not valid on N or have different proofs on N and Z *)
 
 (* None? *)
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index cb8ac3b5b1..0a52d214a2 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -132,7 +132,14 @@ Qed.
 
 End NZOrdAxiomsMod.
 
-Definition Zopp := Zopp.
+Definition Zopp (x : Z) :=
+match x with
+| Z0 => Z0
+| Zpos x => Zneg x
+| Zneg x => Zpos x
+end.
+
+Notation "- x" := (Zopp x) : Z_scope.
 
 Add Morphism Zopp with signature NZE ==> NZE as Zopp_wd.
 Proof.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 5c8b5890d5..9a012b26cf 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -1,48 +1,82 @@
 Require Import NMinus. (* The most complete file for natural numbers *)
-Require Import ZTimesOrder. (* The most complete file for integers *)
+Require Export ZTimesOrder. (* The most complete file for integers *)
 
 Module ZPairsAxiomsMod (Import NAxiomsMod : NAxiomsSig) <: ZAxiomsSig.
 Module Import NPropMod := NMinusPropFunct NAxiomsMod. (* Get all properties of natural numbers *)
-Notation Local N := NZ. (* To remember N without having to use a long qualifying name *)
-Notation Local NE := NZE (only parsing).
-Notation Local plus_wd := NZplus_wd (only parsing).
+
+(* The definitios of functions (NZplus, NZtimes, etc.) will be unfolded by
+the properties functor. Since we don't want Zplus_comm to refer to unfolded
+definitions of equality: fun p1 p2 : NZ => (fst p1 + snd p2) = (fst p2 + snd p1),
+we will provide an extra layer of definitions. *)
+
 Open Local Scope NatIntScope.
+Definition Z := (N * N)%type.
+Definition Z0 : Z := (0, 0).
+Definition Zeq (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)).
+Definition Zsucc (n : Z) : Z := (S (fst n), snd n).
+Definition Zpred (n : Z) : Z := (fst n, S (snd n)).
 
-Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
-Module Export NZAxiomsMod <: NZAxiomsSig.
+(* We do not have Zpred (Zsucc n) = n but only Zpred (Zsucc n) = n. It
+could be possible to consider as canonical only pairs where one of the
+elements is 0, and make all operations convert canonical values into other
+canonical values. In that case, we could get rid of setoids as well as
+arrive at integers as signed natural numbers. *)
+
+Definition Zplus (n m : Z) : Z := ((fst n) + (fst m), (snd n) + (snd m)).
+Definition Zminus (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst m)).
 
-Definition NZ : Set := (NZ * NZ)%type.
-Definition NZE (p1 p2 : NZ) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)).
-Notation Z := NZ (only parsing).
-Notation E := NZE (only parsing).
-Definition NZ0 := (0, 0).
-Definition NZsucc (n : Z) := (S (fst n), snd n).
-Definition NZpred (n : Z) := (fst n, S (snd n)).
-(* We do not have P (S n) = n but only P (S n) == n. It could be possible
-to consider as canonical only pairs where one of the elements is 0, and
-make all operations convert canonical values into other canonical values.
-In that case, we could get rid of setoids as well as arrive at integers as
-signed natural numbers. *)
-Definition NZplus (n m : Z) := ((fst n) + (fst m), (snd n) + (snd m)).
-Definition NZminus (n m : Z) := ((fst n) + (snd m), (snd n) + (fst m)).
 (* Unfortunately, the elements of the pair keep increasing, even during
 subtraction *)
-Definition NZtimes (n m : Z) :=
+
+Definition Ztimes (n m : Z) : Z :=
   ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)).
+Definition Zlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n).
+Definition Zle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n).
 
-Theorem ZE_refl : reflexive Z E.
+Delimit Scope IntScope with Int.
+Bind Scope IntScope with Z.
+Notation "x == y"  := (Zeq x y) (at level 70) : IntScope.
+Notation "x ~= y" := (~ Zeq x y) (at level 70) : IntScope.
+Notation "0" := Z0 : IntScope.
+Notation "1" := (Zsucc Z0) : IntScope.
+Notation "x + y" := (Zplus x y) : IntScope.
+Notation "x - y" := (Zminus x y) : IntScope.
+Notation "x * y" := (Ztimes x y) : IntScope.
+Notation "x < y" := (Zlt x y) : IntScope.
+Notation "x <= y" := (Zle x y) : IntScope.
+Notation "x > y" := (Zlt y x) (only parsing) : IntScope.
+Notation "x >= y" := (Zle y x) (only parsing) : IntScope.
+
+Notation Local N := NZ.
+(* To remember N without having to use a long qualifying name. since NZ will be redefined *)
+Notation Local NE := NZE (only parsing).
+Notation Local plus_wd := NZplus_wd (only parsing).
+
+Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
+Module Export NZAxiomsMod <: NZAxiomsSig.
+
+Definition NZ : Set := Z.
+Definition NZE := Zeq.
+Definition NZ0 := Z0.
+Definition NZsucc := Zsucc.
+Definition NZpred := Zpred.
+Definition NZplus := Zplus.
+Definition NZminus := Zminus.
+Definition NZtimes := Ztimes.
+
+Theorem ZE_refl : reflexive Z Zeq.
 Proof.
-unfold reflexive, E; reflexivity.
+unfold reflexive, Zeq. reflexivity.
 Qed.
 
-Theorem ZE_symm : symmetric Z E.
+Theorem ZE_symm : symmetric Z Zeq.
 Proof.
-unfold symmetric, E; now symmetry.
+unfold symmetric, Zeq; now symmetry.
 Qed.
 
-Theorem ZE_trans : transitive Z E.
+Theorem ZE_trans : transitive Z Zeq.
 Proof.
-unfold transitive, E. intros n m p H1 H2.
+unfold transitive, Zeq. intros n m p H1 H2.
 assert (H3 : (fst n + snd m) + (fst m + snd p) == (fst m + snd n) + (fst p + snd m))
 by now apply plus_wd.
 stepl ((fst n + snd p) + (fst m + snd m)) in H3 by ring.
@@ -50,46 +84,46 @@ stepr ((fst p + snd n) + (fst m + snd m)) in H3 by ring.
 now apply -> plus_cancel_r in H3.
 Qed.
 
-Theorem NZE_equiv : equiv Z E.
+Theorem NZE_equiv : equiv Z Zeq.
 Proof.
 unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_symm].
 Qed.
 
-Add Relation Z E
+Add Relation Z Zeq
  reflexivity proved by (proj1 NZE_equiv)
  symmetry proved by (proj2 (proj2 NZE_equiv))
  transitivity proved by (proj1 (proj2 NZE_equiv))
 as NZE_rel.
 
-Add Morphism (@pair N N) with signature NE ==> NE ==> E as Zpair_wd.
+Add Morphism (@pair N N) with signature NE ==> NE ==> Zeq as Zpair_wd.
 Proof.
-intros n1 n2 H1 m1 m2 H2; unfold E; simpl; rewrite H1; now rewrite H2.
+intros n1 n2 H1 m1 m2 H2; unfold Zeq; simpl; rewrite H1; now rewrite H2.
 Qed.
 
-Add Morphism NZsucc with signature E ==> E as NZsucc_wd.
+Add Morphism NZsucc with signature Zeq ==> Zeq as NZsucc_wd.
 Proof.
-unfold NZsucc, E; intros n m H; simpl.
+unfold NZsucc, Zeq; intros n m H; simpl.
 do 2 rewrite plus_succ_l; now rewrite H.
 Qed.
 
-Add Morphism NZpred with signature E ==> E as NZpred_wd.
+Add Morphism NZpred with signature Zeq ==> Zeq as NZpred_wd.
 Proof.
-unfold NZpred, E; intros n m H; simpl.
+unfold NZpred, Zeq; intros n m H; simpl.
 do 2 rewrite plus_succ_r; now rewrite H.
 Qed.
 
-Add Morphism NZplus with signature E ==> E ==> E as NZplus_wd.
+Add Morphism NZplus with signature Zeq ==> Zeq ==> Zeq as NZplus_wd.
 Proof.
-unfold E, NZplus; intros n1 m1 H1 n2 m2 H2; simpl.
+unfold Zeq, NZplus; intros n1 m1 H1 n2 m2 H2; simpl.
 assert (H3 : (fst n1 + snd m1) + (fst n2 + snd m2) == (fst m1 + snd n1) + (fst m2 + snd n2))
 by now apply plus_wd.
 stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring.
 now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring.
 Qed.
 
-Add Morphism NZminus with signature E ==> E ==> E as NZminus_wd.
+Add Morphism NZminus with signature Zeq ==> Zeq ==> Zeq as NZminus_wd.
 Proof.
-unfold E, NZminus; intros n1 m1 H1 n2 m2 H2; simpl.
+unfold Zeq, NZminus; intros n1 m1 H1 n2 m2 H2; simpl.
 symmetry in H2.
 assert (H3 : (fst n1 + snd m1) + (fst m2 + snd n2) == (fst m1 + snd n1) + (fst n2 + snd m2))
 by now apply plus_wd.
@@ -97,9 +131,9 @@ stepl (fst n1 + snd m1 + (fst m2 + snd n2)) by ring.
 now stepr (fst m1 + snd n1 + (fst n2 + snd m2)) by ring.
 Qed.
 
-Add Morphism NZtimes with signature E ==> E ==> E as NZtimes_wd.
+Add Morphism NZtimes with signature Zeq ==> Zeq ==> Zeq as NZtimes_wd.
 Proof.
-unfold NZtimes, E; intros n1 m1 H1 n2 m2 H2; simpl.
+unfold NZtimes, Zeq; intros n1 m1 H1 n2 m2 H2; simpl.
 stepl (fst n1 * fst n2 + (snd n1 * snd n2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
 stepr (fst n1 * snd n2 + (fst m1 * fst m2 + snd m1 * snd m2 + snd n1 * fst n2)) by ring.
 apply plus_times_repl_pair with (n := fst m2) (m := snd m2); [| now idtac].
@@ -117,39 +151,20 @@ apply plus_times_repl_pair with (n := fst m1) (m := snd m1); [| now idtac].
 ring.
 Qed.
 
-Delimit Scope IntScope with Int.
-Bind Scope IntScope with NZ.
-Open Local Scope IntScope.
-Notation "x == y"  := (NZE x y) (at level 70) : IntScope.
-Notation "x ~= y" := (~ NZE x y) (at level 70) : IntScope.
-Notation "0" := NZ0 : IntScope.
-Notation "'S'" := NZsucc : IntScope.
-Notation "'P'" := NZpred : IntScope.
-Notation "1" := (S 0) : IntScope.
-Notation "x + y" := (NZplus x y) : IntScope.
-Notation "x - y" := (NZminus x y) : IntScope.
-Notation "x * y" := (NZtimes x y) : IntScope.
-
-Theorem NZpred_succ : forall n : Z, P (S n) == n.
-Proof.
-unfold NZpred, NZsucc, E; intro n; simpl.
-rewrite plus_succ_l; now rewrite plus_succ_r.
-Qed.
-
 Section Induction.
 Open Scope NatIntScope. (* automatically closes at the end of the section *)
 Variable A : Z -> Prop.
-Hypothesis A_wd : predicate_wd E A.
+Hypothesis A_wd : predicate_wd Zeq A.
 
-Add Morphism A with signature E ==> iff as A_morph.
+Add Morphism A with signature Zeq ==> iff as A_morph.
 Proof.
 exact A_wd.
 Qed.
 
 Theorem NZinduction :
-  A 0 -> (forall n : Z, A n <-> A (S n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *)
+  A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *)
 Proof.
-intros A0 AS n; unfold NZ0, NZsucc, predicate_wd, fun_wd, E in *.
+intros A0 AS n; unfold NZ0, Zsucc, predicate_wd, fun_wd, Zeq in *.
 destruct n as [n m].
 cut (forall p : N, A (p, 0)); [intro H1 |].
 cut (forall p : N, A (0, p)); [intro H2 |].
@@ -166,51 +181,56 @@ Qed.
 
 End Induction.
 
+(* Time to prove theorems in the language of Z *)
+
+Open Local Scope IntScope.
+
+Theorem NZpred_succ : forall n : Z, Zpred (Zsucc n) == n.
+Proof.
+unfold NZpred, NZsucc, Zeq; intro n; simpl.
+rewrite plus_succ_l; now rewrite plus_succ_r.
+Qed.
+
 Theorem NZplus_0_l : forall n : Z, 0 + n == n.
 Proof.
-intro n; unfold NZplus, E; simpl. now do 2 rewrite plus_0_l.
+intro n; unfold NZplus, Zeq; simpl. now do 2 rewrite plus_0_l.
 Qed.
 
-Theorem NZplus_succ_l : forall n m : Z, (S n) + m == S (n + m).
+Theorem NZplus_succ_l : forall n m : Z, (Zsucc n) + m == Zsucc (n + m).
 Proof.
-intros n m; unfold NZplus, E; simpl. now do 2 rewrite plus_succ_l.
+intros n m; unfold NZplus, Zeq; simpl. now do 2 rewrite plus_succ_l.
 Qed.
 
 Theorem NZminus_0_r : forall n : Z, n - 0 == n.
 Proof.
-intro n; unfold NZminus, E; simpl. now do 2 rewrite plus_0_r.
+intro n; unfold NZminus, Zeq; simpl. now do 2 rewrite plus_0_r.
 Qed.
 
-Theorem NZminus_succ_r : forall n m : Z, n - (S m) == P (n - m).
+Theorem NZminus_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m).
 Proof.
-intros n m; unfold NZminus, E; simpl. symmetry; now rewrite plus_succ_r.
+intros n m; unfold NZminus, Zeq; simpl. symmetry; now rewrite plus_succ_r.
 Qed.
 
 Theorem NZtimes_0_r : forall n : Z, n * 0 == 0.
 Proof.
-intro n; unfold NZtimes, E; simpl.
+intro n; unfold NZtimes, Zeq; simpl.
 repeat rewrite times_0_r. now rewrite plus_assoc.
 Qed.
 
-Theorem NZtimes_succ_r : forall n m : Z, n * (S m) == n * m + n.
+Theorem NZtimes_succ_r : forall n m : Z, n * (Zsucc m) == n * m + n.
 Proof.
-intros n m; unfold NZtimes, NZsucc, E; simpl.
+intros n m; unfold NZtimes, NZsucc, Zeq; simpl.
 do 2 rewrite times_succ_r. ring.
 Qed.
 
 End NZAxiomsMod.
 
-Definition NZlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n).
-Definition NZle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n).
-
-Notation "x < y" := (NZlt x y) : IntScope.
-Notation "x <= y" := (NZle x y) : IntScope.
-Notation "x > y" := (NZlt y x) (only parsing) : IntScope.
-Notation "x >= y" := (NZle y x) (only parsing) : IntScope.
+Definition NZlt := Zlt.
+Definition NZle := Zle.
 
-Add Morphism NZlt with signature E ==> E ==> iff as NZlt_wd.
+Add Morphism NZlt with signature Zeq ==> Zeq ==> iff as NZlt_wd.
 Proof.
-unfold NZlt, E; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H.
+unfold NZlt, Zlt, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H.
 stepr (snd m1 + fst m2) by apply plus_comm.
 apply (plus_lt_repl_pair (fst n1) (snd n1)); [| assumption].
 stepl (snd m2 + fst n1) by apply plus_comm.
@@ -227,58 +247,58 @@ now stepl (fst m1 + snd m2) by apply plus_comm.
 stepl (fst n2 + snd m2) by apply plus_comm. now stepr (fst m2 + snd n2) by apply plus_comm.
 Qed.
 
-Open Local Scope IntScope.
-
-Add Morphism NZle with signature E ==> E ==> iff as NZle_wd.
+Add Morphism NZle with signature Zeq ==> Zeq ==> iff as NZle_wd.
 Proof.
-unfold NZle, E; intros n1 m1 H1 n2 m2 H2; simpl.
-do 2 rewrite le_lt_or_eq. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2).
-fold (n1 == n2) (m1 == m2); fold (n1 == m1) in H1; fold (n2 == m2) in H2.
+unfold NZle, Zle, Zeq; intros n1 m1 H1 n2 m2 H2; simpl.
+do 2 rewrite le_lt_or_eq. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2)%Int.
+fold (n1 == n2)%Int (m1 == m2)%Int; fold (n1 == m1)%Int in H1; fold (n2 == m2)%Int in H2.
 now rewrite H1, H2.
 Qed.
 
+Open Local Scope IntScope.
+
 Theorem NZle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m.
 Proof.
-intros n m; unfold NZlt, NZle, E; simpl. apply le_lt_or_eq.
+intros n m; unfold Zlt, Zle, Zeq; simpl. apply le_lt_or_eq.
 Qed.
 
 Theorem NZlt_irrefl : forall n : Z, ~ (n < n).
 Proof.
-intros n; unfold NZlt, E; simpl. apply lt_irrefl.
+intros n; unfold Zlt, Zeq; simpl. apply lt_irrefl.
 Qed.
 
-Theorem NZlt_succ_le : forall n m : Z, n < (S m) <-> n <= m.
+Theorem NZlt_succ_le : forall n m : Z, n < (Zsucc m) <-> n <= m.
 Proof.
-intros n m; unfold NZlt, NZle, E; simpl. rewrite plus_succ_l; apply lt_succ_le.
+intros n m; unfold Zlt, Zle, Zeq; simpl. rewrite plus_succ_l; apply lt_succ_le.
 Qed.
 
 End NZOrdAxiomsMod.
 
-Definition Zopp (n : Z) := (snd n, fst n).
+Definition Zopp (n : Z) : Z := (snd n, fst n).
 
-Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope.
+Notation "- x" := (Zopp x) : IntScope.
 
-Add Morphism Zopp with signature E ==> E as Zopp_wd.
+Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd.
 Proof.
-unfold E; intros n m H; simpl. symmetry.
+unfold Zeq; intros n m H; simpl. symmetry.
 stepl (fst n + snd m) by apply plus_comm.
 now stepr (fst m + snd n) by apply plus_comm.
 Qed.
 
 Open Local Scope IntScope.
 
-Theorem Zsucc_pred : forall n : Z, S (P n) == n.
+Theorem Zsucc_pred : forall n : Z, Zsucc (Zpred n) == n.
 Proof.
-intro n; unfold NZsucc, NZpred, E; simpl.
+intro n; unfold Zsucc, Zpred, Zeq; simpl.
 rewrite plus_succ_l; now rewrite plus_succ_r.
 Qed.
 
 Theorem Zopp_0 : - 0 == 0.
 Proof.
-unfold Zopp, E; simpl. now rewrite plus_0_l.
+unfold Zopp, Zeq; simpl. now rewrite plus_0_l.
 Qed.
 
-Theorem Zopp_succ : forall n, - (S n) == P (- n).
+Theorem Zopp_succ : forall n, - (Zsucc n) == Zpred (- n).
 Proof.
 reflexivity.
 Qed.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 5c6369fe49..cb3dd3093f 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -44,6 +44,13 @@ Proof.
 intros n m H1 H2; rewrite H2 in H1; false_hyp H1 NZlt_irrefl.
 Qed.
 
+Theorem NZlt_le_neq : forall n m : NZ, n < m <-> n <= m /\ n ~= m.
+Proof.
+intros n m; split; [intro H | intros [H1 H2]].
+split. le_less. now apply NZlt_neq.
+le_elim H1. assumption. false_hyp H1 H2.
+Qed.
+
 Theorem NZle_refl : forall n : NZ, n <= n.
 Proof.
 intro; now le_equal.
diff --git a/theories/Numbers/NatInt/NZPlusOrder.v b/theories/Numbers/NatInt/NZPlusOrder.v
deleted file mode 100644
index 6368fa5578..0000000000
--- a/theories/Numbers/NatInt/NZPlusOrder.v
+++ /dev/null
@@ -1,67 +0,0 @@
-Require Export NZPlus.
-Require Export NZOrder.
-
-Module NZPlusOrderPropFunct
-  (Import NZPlusMod : NZPlusSig)
-  (Import NZOrderMod : NZOrderSig with Module NZBaseMod := NZPlusMod.NZBaseMod).
-
-Module Export NZPlusPropMod := NZPlusPropFunct NZPlusMod.
-Module Export NZOrderPropMod := NZOrderPropFunct NZOrderMod.
-Open Local Scope NatIntScope.
-
-Theorem NZplus_lt_mono_l : forall n m p, 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.
-Qed.
-
-Theorem NZplus_lt_mono_r : forall n m p, 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.
-Qed.
-
-Theorem NZplus_lt_mono : forall n m p q, 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].
-Qed.
-
-Theorem NZplus_le_mono_l : forall n m p, 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.
-Qed.
-
-Theorem NZplus_le_mono_r : forall n m p, 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.
-Qed.
-
-Theorem NZplus_le_mono : forall n m p q, 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].
-Qed.
-
-Theorem NZplus_lt_le_mono : forall n m p q, 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].
-Qed.
-
-Theorem NZplus_le_lt_mono : forall n m p q, 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].
-Qed.
-
-End NZPlusOrderPropFunct.
-
diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v
index 6f702067da..2f3cf678b9 100644
--- a/theories/Numbers/NatInt/NZTimesOrder.v
+++ b/theories/Numbers/NatInt/NZTimesOrder.v
@@ -61,6 +61,37 @@ apply NZle_lt_trans with (m + p);
 [now apply -> NZplus_le_mono_r | now apply -> NZplus_lt_mono_l].
 Qed.
 
+Theorem NZplus_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.
+Qed.
+
+Theorem NZplus_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.
+Qed.
+
+Theorem NZplus_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.
+Qed.
+
+Theorem NZplus_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.
+Qed.
+
+Theorem NZlt_plus_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.
+Qed.
+
+Theorem NZlt_plus_pos_r : forall n m : NZ, 0 < n -> m < m + n.
+Proof.
+intros; rewrite NZplus_comm; now apply NZlt_plus_pos_l.
+Qed.
+
 Theorem NZle_lt_plus_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].
@@ -75,7 +106,7 @@ pose proof (NZplus_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_lt : forall n m p q : NZ, n <= m -> p + m <= q + n -> p <= q.
+Theorem NZle_le_plus_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.
@@ -370,4 +401,14 @@ elimtype False; now apply (NZlt_asymm (n * m) 0).
 now apply NZtimes_neg_pos. now apply NZtimes_pos_neg.
 Qed.
 
+Theorem NZtimes_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
+Proof.
+intros n m H. apply -> NZlt_le_succ 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.
+now apply <- NZlt_le_succ.
+apply NZplus_pos_pos; now apply NZlt_succ_r.
+Qed.
+
 End NZTimesOrderPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index f62b5ecb2a..7c2610ccc6 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -25,6 +25,9 @@ Proof NZlt_le_incl.
 Theorem lt_neq : forall n m : N, n < m -> n ~= m.
 Proof NZlt_neq.
 
+Theorem lt_le_neq : forall n m : N, n < m <-> n <= m /\ n ~= m.
+Proof NZlt_le_neq.
+
 Theorem le_refl : forall n : N, n <= n.
 Proof NZle_refl.
 
diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NPlusOrder.v
deleted file mode 100644
index c4640858e0..0000000000
--- a/theories/Numbers/Natural/Abstract/NPlusOrder.v
+++ /dev/null
@@ -1,87 +0,0 @@
-Require Export NPlus.
-Require Export NOrder.
-Require Import NZPlusOrder.
-
-Module NPlusOrderPropFunct
-  (Import NPlusMod : NPlusSig)
-  (Import NOrderMod : NOrderSig with Module NAxiomsMod := NPlusMod.NAxiomsMod).
-Module Export NPlusPropMod := NPlusPropFunct NPlusMod.
-Module Export NOrderPropMod := NOrderPropFunct NOrderMod.
-Module Export NZPlusOrderPropMod := NZPlusOrderPropFunct NZPlusMod NZOrderMod.
-Open Local Scope NatScope.
-
-(* Print All locks up here !!! *)
-Theorem lt_plus_trans : forall n m p, n < m -> n < m + p.
-Proof.
-intros n m p; induct p.
-now rewrite plus_0_r.
-intros x IH H.
-rewrite plus_succ_r. apply lt_closed_succ. apply IH; apply H.
-Qed.
-
-Theorem plus_lt_compat_l : forall n m p, n < m -> p + n < p + m.
-Proof.
-intros n m p H; induct p.
-do 2 rewrite plus_0_l; assumption.
-intros x IH. do 2 rewrite plus_succ_l. now apply <- lt_resp_succ.
-Qed.
-
-Theorem plus_lt_compat_r : forall n m p, n < m -> n + p < m + p.
-Proof.
-intros n m p H; rewrite plus_comm.
-set (k := p + n); rewrite plus_comm; unfold k; clear k.
-now apply plus_lt_compat_l.
-Qed.
-
-Theorem plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
-Proof.
-intros n m p q H1 H2.
-apply lt_trans with (m := m + p);
-[now apply plus_lt_compat_r | now apply plus_lt_compat_l].
-Qed.
-
-Theorem plus_lt_cancel_l : forall p n m, p + n < p + m <-> n < m.
-Proof.
-intros p n m; induct p.
-now do 2 rewrite plus_0_l.
-intros p IH.
-do 2 rewrite plus_succ_l. now rewrite lt_resp_succ.
-Qed.
-
-Theorem plus_lt_cancel_r : forall p n m, n + p < m + p <-> n < m.
-Proof.
-intros p n m;
-setoid_replace (n + p) with (p + n) by apply plus_comm;
-setoid_replace (m + p) with (p + m) by apply plus_comm;
-apply plus_lt_cancel_l.
-Qed.
-
-(* The following property is similar to plus_repl_pair in NPlus.v
-and 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 + u < m + v -> n + m' == n' + m -> n' + u < m' + v.
-Proof.
-intros n m n' m' u v H1 H2.
-apply <- (plus_lt_cancel_r (n + m')) in H1.
-set (k := n + m') in H1 at 2; rewrite H2 in H1; unfold k in H1; clear k.
-rewrite <- plus_assoc in H1.
-setoid_replace (m + v + (n + m')) with (n + m' + (m + v)) in H1 by apply plus_comm.
-rewrite <- plus_assoc in H1. apply -> plus_lt_cancel_l in H1.
-rewrite plus_assoc in H1. setoid_replace (m + v) with (v + m) in H1 by apply plus_comm.
-rewrite plus_assoc in H1. apply -> plus_lt_cancel_r in H1.
-now rewrite plus_comm in H1.
-Qed.
-
-Theorem plus_gt_succ :
-  forall n m p, S p < n + m -> (exists n', n == S n') \/ (exists m', m == S m').
-Proof.
-intros n m p H.
-apply <- lt_le_succ in H.
-apply lt_exists_pred in H. destruct H as [q H].
-now apply plus_eq_succ in H.
-Qed.
-
-End NPlusOrderProperties.
-
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v
index 2dbfd8f977..dc1b977aa4 100644
--- a/theories/Numbers/Natural/Abstract/NTimesOrder.v
+++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v
@@ -28,22 +28,31 @@ Proof NZplus_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 plus_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n + m.
+Proof NZplus_pos_pos.
+
+Theorem lt_plus_pos_l : forall n m : N, 0 < n -> m < n + m.
+Proof NZlt_plus_pos_l.
+
+Theorem lt_plus_pos_r : forall n m : N, 0 < n -> m < m + n.
+Proof NZlt_plus_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 lt_le_plus_lt : forall n m p q : N, n < m -> p + m <= q + n -> p < q.
 Proof NZlt_le_plus_lt.
 
-Theorem le_le_plus_lt : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q.
-Proof NZle_le_plus_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 plus_lt_cases : forall n m p q : N, n + m < p + q -> n < p \/ m < q.
 Proof NZplus_lt_cases.
 
-Theorem plus_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q.
+Theorem plus_le_cases : forall n m p q : N, n + m <= p + q -> n <= p \/ m <= q.
 Proof NZplus_le_cases.
 
-Theorem plus_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m.
+Theorem plus_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m.
 Proof NZplus_pos_cases.
 
 (** Theorems true for natural numbers *)
@@ -55,17 +64,25 @@ rewrite plus_0_r; le_equal.
 intros m IH. rewrite plus_succ_r; now apply le_le_succ.
 Qed.
 
-Theorem lt_plus_r : forall n m : N, m ~= 0 -> n < n + m.
+Theorem lt_lt_plus_r : forall n m p : N, n < m -> n < m + p.
 Proof.
-intros n m; cases m.
-intro H; elimtype False; now apply H.
-intros. rewrite plus_succ_r. apply <- lt_succ_le. apply le_plus_r.
+intros n m p H; rewrite <- (plus_0_r n).
+apply plus_lt_le_mono; [assumption | apply le_0_l].
 Qed.
 
-Theorem lt_lt_plus : forall n m p : N, n < m -> n < m + p.
+Theorem lt_lt_plus_l : forall n m p : N, n < m -> n < p + m.
 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; rewrite plus_comm; apply lt_lt_plus_r.
+Qed.
+
+Theorem plus_pos_l : forall n m : N, 0 < n -> 0 < n + m.
+Proof.
+intros; apply NZplus_pos_nonneg. assumption. apply le_0_l.
+Qed.
+
+Theorem plus_pos_r : forall n m : N, 0 < m -> 0 < n + m.
+Proof.
+intros; apply NZplus_nonneg_pos. apply le_0_l. assumption.
 Qed.
 
 (* The following property is similar to plus_repl_pair in NPlus.v
@@ -123,7 +140,7 @@ Proof.
 intros; apply NZtimes_le_mono; try assumption; apply le_0_l.
 Qed.
 
-Theorem times_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m.
+Theorem Ztimes_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m.
 Proof NZtimes_pos_pos.
 
 Theorem times_eq_0 : forall n m : N, n * m == 0 -> n == 0 \/ m == 0.
@@ -132,11 +149,14 @@ Proof NZtimes_eq_0.
 Theorem times_neq_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
 Proof NZtimes_neq_0.
 
+Theorem times_2_mono_l : forall n m : N, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
+Proof NZtimes_2_mono_l.
+
 Theorem times_pos : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0.
 Proof.
 intros n m; split; [intro H | intros [H1 H2]].
 apply -> NZtimes_pos in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r.
-now apply times_pos_pos.
+now apply NZtimes_pos_pos.
 Qed.
 
 End NTimesOrderPropFunct.