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

3 files changed, 49 insertions, 68 deletions

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.