From b12e5e4b61aabea94129b70f88967b2d0b84c2b6 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 10 Oct 2019 12:36:03 +0000
Subject: Qround: do not use “omega”

---
 theories/QArith/Qround.v | 7 ++++---
 1 file 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.
-- 
cgit v1.2.3