summaryrefslogtreecommitdiff
path: root/theories/ZArith
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith')
-rw-r--r--theories/ZArith/Zorder.v14
1 files changed, 10 insertions, 4 deletions
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 55d4d958..27eb02cd 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Zorder.v,v 1.6.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
+(*i $Id: Zorder.v,v 1.6.2.3 2005/03/29 15:35:12 herbelin Exp $ i*)
(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
@@ -849,12 +849,15 @@ intros p H1; unfold Zgt in |- *; pattern 0 at 2 in |- *;
intros p H; discriminate H.
Qed.
-Lemma Zmult_lt_O_compat : forall n m:Z, 0 < n -> 0 < m -> 0 < n * m.
+Lemma Zmult_lt_0_compat : forall n m:Z, 0 < n -> 0 < m -> 0 < n * m.
intros a b apos bpos.
apply Zgt_lt.
apply Zmult_gt_0_compat; try apply Zlt_gt; assumption.
Qed.
+(* For compatibility *)
+Notation Zmult_lt_O_compat := Zmult_lt_0_compat (only parsing).
+
Lemma Zmult_gt_0_le_0_compat : forall n m:Z, n > 0 -> 0 <= m -> 0 <= m * n.
Proof.
intros x y H1 H2; apply Zmult_le_0_compat; trivial.
@@ -958,8 +961,11 @@ intros n m H; apply Zplus_lt_reg_l with (p := m); rewrite Zplus_minus;
assumption.
Qed.
-Lemma Zlt_O_minus_lt : forall n m:Z, 0 < n - m -> m < n.
+Lemma Zlt_0_minus_lt : forall n m:Z, 0 < n - m -> m < n.
Proof.
intros n m H; apply Zplus_lt_reg_l with (p := - m); rewrite Zplus_opp_l;
rewrite Zplus_comm; exact H.
-Qed. \ No newline at end of file
+Qed.
+
+(* For compatibility *)
+Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing).