From b74a68a56164f952345ba083f42b95eaaa37355e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Nov 2003 11:56:54 +0000
Subject: Des oublis

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

diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index ccfb9855bb..905466b629 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -741,9 +741,26 @@ Apply Zmult_reg_right with z.
   Intro. Rewrite H0 in Hz. Contradiction (Zgt_antirefl `0`).
 Assumption.
 Qed.
+V7only [Notation Zle_mult_simpl := Zle_Zmult_right2.
+(* Zle_mult_simpl 
+ : (a,b,c:Z)(Zgt c ZERO)->(Zle (Zmult a c) (Zmult b c))->(Zle a b). *)
+].
 
 V7only [Unset Implicit Arguments.].
 
+Lemma Zge_mult_simpl 
+ : (a,b,c:Z) (Zgt c ZERO)->(Zge (Zmult a c) (Zmult b c))->(Zge a b).
+Intros a b c H1 H2; Apply Zle_ge; Apply Zle_mult_simpl with c; Trivial.
+Apply Zge_le; Trivial.
+Qed.
+
+Lemma Zgt_mult_simpl 
+ : (a,b,c:Z) (Zgt c ZERO)->(Zgt (Zmult a c) (Zmult b c))->(Zgt a b).
+Intros a b c H1 H2; Apply Zlt_gt; Apply Zlt_Zmult_right2 with c; Trivial.
+Apply Zgt_lt; Trivial.
+Qed.
+
+
 (** Compatibility of multiplication by a positive wrt to being positive *)
 
 Theorem Zle_ZERO_mult : 
-- 
cgit v1.2.3