From 0f70e9e4bea59ebb4690976425609a7b204680bb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 24 Mar 2005 16:28:19 +0000
Subject: Missing translating a 'O' into a '0'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6884 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/Zorder.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index a0b8ad2f3d..779cd67634 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -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.
@@ -962,4 +965,4 @@ Lemma Zlt_O_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.
-- 
cgit v1.2.3