diff options
| author | Vincent Laporte | 2019-10-28 12:53:05 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-11-25 08:40:38 +0000 |
| commit | c997e97897712e4e55cb4b0238f176bd57ff9374 (patch) | |
| tree | 9b57edbb777692bfc34da79fe1bfec8b65d4b96e | |
| parent | acf89f2db9a3c87afaceda20135539b5c4013585 (diff) | |
zify: explicitly use “lia”
| -rw-r--r-- | plugins/micromega/ZifyComparison.v | 9 |
1 files changed, 5 insertions, 4 deletions
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 := |