3 files changed, 36 insertions, 100 deletions

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.