diff options
| author | Emilio Jesus Gallego Arias | 2019-11-29 17:12:16 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-11-29 17:12:16 +0100 |
| commit | 37b1348d54df2d65389987e8bd920f9e1b275c44 (patch) | |
| tree | f651a6c919c078744af13fed4eaff6e20e54389b /plugins/micromega | |
| parent | 18ad1b309bbdcf8aa4cc12b024b88007dfd9c14f (diff) | |
| parent | ed89ceb71efa910764290e4017c0ca9cb829eb7c (diff) | |
Merge PR #11076: Remove all remaining calls to “omega” from the standard library
Reviewed-by: ejgallego
Diffstat (limited to 'plugins/micromega')
| -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 := |