diff options
| author | Vincent Laporte | 2019-10-28 12:51:30 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-11-25 08:40:38 +0000 |
| commit | 791ea687b5bbcca4cfc3dc53a57a3ff10037229e (patch) | |
| tree | af28798952a30248e2df058c646b12ce4ada2f1d | |
| parent | 9210c5da6b1057194fd73acd5b26ece57dcfa477 (diff) | |
PermutEq: use “lia” rather than “omega”
| -rw-r--r-- | theories/Sorting/PermutEq.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v index 8e8f05dabc..4feeb9bfff 100644 --- a/theories/Sorting/PermutEq.v +++ b/theories/Sorting/PermutEq.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation Omega. +Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation Lia. Set Implicit Arguments. @@ -85,7 +85,7 @@ Section Perm. rewrite multiplicity_NoDup in H, H0. generalize (H a) (H0 a) (H1 a); clear H H0 H1. do 2 rewrite multiplicity_In. - destruct 3; omega. + destruct 3; lia. Qed. (** Permutation is compatible with In. *) |