diff options
Diffstat (limited to 'theories/ZArith/Zorder.v')
-rw-r--r-- | theories/ZArith/Zorder.v | 32 |
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). |