diff options
| author | Vincent Laporte | 2019-10-28 13:55:35 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-10-31 14:10:58 +0000 |
| commit | fcebe5a64bb253862e52503b7d4dd6c4c1aebcdf (patch) | |
| tree | bafa6155d964be6996a2b265a3cdd17ecd0ed41f | |
| parent | 9151bddfc935a706c6e21516996bcee9cbdbd71d (diff) | |
QArith: only depend on ZArith_base
| -rw-r--r-- | theories/QArith/QArith_base.v | 2 | ||||
| -rw-r--r-- | theories/QArith/Qround.v | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 54d35cded2..4239943d03 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Export ZArith. +Require Export ZArith_base. Require Export ZArithRing. Require Export Morphisms Setoid Bool. diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index 8d68038582..35f113e226 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -9,6 +9,7 @@ (************************************************************************) Require Import QArith. +Import Zdiv. Lemma Qopp_lt_compat: forall p q : Q, p < q -> - q < - p. Proof. @@ -38,7 +39,7 @@ Proof. intros z. unfold Qceiling. simpl. -rewrite Zdiv_1_r. +rewrite Z.div_1_r. apply Z.opp_involutive. Qed. @@ -50,8 +51,7 @@ unfold Qle. simpl. replace (n*1)%Z with n by ring. rewrite Z.mul_comm. -apply Z_mult_div_ge. -auto with *. +now apply Z.mul_div_le. Qed. Hint Resolve Qfloor_le : qarith. |