diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-03-24 16:28:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-03-24 16:28:19 +0000 |
| commit | 0f70e9e4bea59ebb4690976425609a7b204680bb (patch) | |
| tree | ca535de13b577659a58e2fad64487fb879d67d21 /theories/ZArith/Zorder.v | |
| parent | bf7592d6ea7bd0e485d02c45f25c29b82c2d43c5 (diff) | |
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
Diffstat (limited to 'theories/ZArith/Zorder.v')
| -rw-r--r-- | theories/ZArith/Zorder.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index a0b8ad2f3..779cd6763 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. |