1 files changed, 29 insertions, 3 deletions

diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 47490be6..425aa83b 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -5,9 +5,9 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*i $Id: Zorder.v 9302 2006-10-27 21:21:17Z barras $ i*)
+(*i $Id: Zorder.v 10291 2007-11-06 02:18:53Z letouzey $ i*)
 
-(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
 
 Require Import BinPos.
 Require Import BinInt.
@@ -549,7 +549,7 @@ Hint Immediate Zeq_le: zarith.
 
 (** Transitivity using successor *)
 
-Lemma Zge_trans_succ : forall n m p:Z, Zsucc n > m -> m > p -> n > p.
+Lemma Zgt_trans_succ : forall n m p:Z, Zsucc n > m -> m > p -> n > p.
 Proof.
   intros n m p H1 H2; apply Zle_gt_trans with (m := m);
     [ apply Zgt_succ_le; assumption | assumption ].
@@ -997,5 +997,31 @@ Proof.
     rewrite <- Zplus_assoc; rewrite Zplus_opp_l; rewrite Zplus_0_r; exact H. 
 Qed.
 
+Lemma Zmult_lt_compat:
+  forall n m p q : Z, 0 <= n < p -> 0 <= m < q -> n * m < p * q.
+Proof.
+  intros n m p q (H1, H2) (H3,H4).
+  assert (0<p) by (apply Zle_lt_trans with n; auto).
+  assert (0<q) by (apply Zle_lt_trans with m; auto).
+  case Zle_lt_or_eq with (1 := H1); intros H5; auto with zarith.
+  case Zle_lt_or_eq with (1 := H3); intros H6; auto with zarith.
+  apply Zlt_trans with (n * q).
+  apply Zmult_lt_compat_l; auto.
+  apply Zmult_lt_compat_r; auto with zarith.
+  rewrite <- H6; rewrite Zmult_0_r; apply Zmult_lt_0_compat; auto with zarith.
+  rewrite <- H5; simpl; apply Zmult_lt_0_compat; auto with zarith.
+Qed.
+
+Lemma Zmult_lt_compat2: 
+  forall n m p q : Z, 0 < n <= p -> 0 < m < q -> n * m < p * q.
+Proof.
+  intros n m p q (H1, H2) (H3, H4).
+  apply Zle_lt_trans with (p * m).
+  apply Zmult_le_compat_r; auto.
+  apply Zlt_le_weak; auto.
+  apply Zmult_lt_compat_l; auto.
+  apply Zlt_le_trans with n; auto.
+Qed.
+
 (** For compatibility *)
 Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing).