From c997e97897712e4e55cb4b0238f176bd57ff9374 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 28 Oct 2019 12:53:05 +0000
Subject: zify: explicitly use “lia”

---
 plugins/micromega/ZifyComparison.v | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/ZifyComparison.v b/plugins/micromega/ZifyComparison.v
index 8a8b40ded8..df75cf2c05 100644
--- a/plugins/micromega/ZifyComparison.v
+++ b/plugins/micromega/ZifyComparison.v
@@ -9,7 +9,8 @@
 (************************************************************************)
 
 Require Import Bool ZArith.
-Require Import ZifyClasses.
+Require Import Zify ZifyClasses.
+Require Import Lia.
 Local Open Scope Z_scope.
 
 (** [Z_of_comparison] is the injection function for comparison *)
@@ -64,11 +65,11 @@ Proof.
   intros.
   destruct (x ?= y) eqn:C; simpl.
   - rewrite Z.compare_eq_iff in C.
-    intuition.
+    lia.
   - rewrite Z.compare_lt_iff in C.
-    intuition.
+    lia.
   - rewrite Z.compare_gt_iff in C.
-    intuition.
+    lia.
 Qed.
 
 Instance ZcompareSpec : BinOpSpec ZcompareZ :=
-- 
cgit v1.2.3