diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-06 11:56:54 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-06 11:56:54 +0000 |
| commit | b74a68a56164f952345ba083f42b95eaaa37355e (patch) | |
| tree | 05550cde9f06dd4d6de2d6b25d8cb1574fa05deb /theories/ZArith/Zorder.v | |
| parent | 9d78f6178a9ffcca63de531393bfbb8d02535557 (diff) | |
Des oublis
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4819 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zorder.v')
| -rw-r--r-- | theories/ZArith/Zorder.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index ccfb9855b..905466b62 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 : |