From 87e2bd27055db7827ab5d5a677e3c6fc876685c6 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 28 Oct 2019 12:52:51 +0000
Subject: lra: use “lia” rather than “omega”

---
 plugins/micromega/RMicromega.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index 3651b54ed8..6c1852acbf 100644
--- a/plugins/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.v
@@ -22,6 +22,7 @@ Require Import QArith.
 Require Import Qfield.
 Require Import Qreals.
 Require Import DeclConstant.
+Require Import Lia.
 
 Require Setoid.
 (*Declare ML Module "micromega_plugin".*)
@@ -192,7 +193,7 @@ Proof.
   destruct z ; try congruence.
   compute. congruence.
   compute. congruence.
-  generalize (Zle_0_nat n). auto with zarith.
+  generalize (Zle_0_nat n). auto using Z.le_ge.
 Qed.
 
 Definition CInvR0 (r : Rcst) := Qeq_bool (Q_of_Rcst r) (0 # 1).
@@ -333,7 +334,7 @@ Proof.
       apply Qeq_bool_eq in C2.
       rewrite C2.
       simpl.
-      rewrite Qpower0 by auto with zarith.
+      rewrite Qpower0 by lia.
       apply Q2R_0.
     + rewrite Q2RpowerRZ.
       rewrite IHc.
@@ -341,7 +342,7 @@ Proof.
       rewrite andb_false_iff in C.
       destruct C.
       simpl. apply Z.ltb_ge in H.
-      auto with zarith.
+      lia.
       left ; apply Qeq_bool_neq; auto.
     + simpl.
       rewrite <- IHc.
-- 
cgit v1.2.3