diff options
| author | Vincent Laporte | 2019-10-10 12:36:03 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-10-22 06:38:21 +0000 |
| commit | b12e5e4b61aabea94129b70f88967b2d0b84c2b6 (patch) | |
| tree | 9d3f1722b90a7eff740b60b9d86618238ebbc111 | |
| parent | 99ac4ab65c90e7b41aea255625f81d26da045ff9 (diff) | |
Qround: do not use “omega”
| -rw-r--r-- | theories/QArith/Qround.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index af5c471d5d..8d68038582 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -13,7 +13,8 @@ Require Import QArith. Lemma Qopp_lt_compat: forall p q : Q, p < q -> - q < - p. Proof. intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl. -rewrite !Z.mul_opp_l; omega. +rewrite !Z.mul_opp_l. +apply Z.opp_lt_mono. Qed. Hint Resolve Qopp_lt_compat : qarith. @@ -38,7 +39,7 @@ intros z. unfold Qceiling. simpl. rewrite Zdiv_1_r. -auto with *. +apply Z.opp_involutive. Qed. Lemma Qfloor_le : forall x, Qfloor x <= x. @@ -119,7 +120,7 @@ Lemma Qceiling_resp_le : forall x y, x <= y -> (Qceiling x <= Qceiling y)%Z. Proof. intros x y Hxy. unfold Qceiling. -cut (Qfloor (-y) <= Qfloor (-x))%Z; auto with *. +rewrite <- Z.opp_le_mono; auto with qarith. Qed. Hint Resolve Qceiling_resp_le : qarith. |