diff options
Diffstat (limited to 'theories')
| -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 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. |