Merge PR #11076: Remove all remaining calls to “omega” from the standard library

Reviewed-by: ejgallego

16 files changed, 81 insertions, 88 deletions

diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index 3ad5bc9f2d..b90e44eed8 100644
--- a/plugins/btauto/Algebra.v
+++ b/plugins/btauto/Algebra.v
@@ -1,4 +1,4 @@
-Require Import Bool PArith DecidableClass Ring Omega Lia.
+Require Import Bool PArith DecidableClass Ring Lia.
 
 Ltac bool :=
 repeat match goal with
@@ -359,8 +359,8 @@ intros k p var1 var2 Hvar Hv; revert var1 var2 Hvar.
 induction Hv; intros var1 var2 Hvar; simpl; [now auto|].
 rewrite Hvar; [|now auto]; erewrite (IHHv1 var1 var2).
   + erewrite (IHHv2 var1 var2); [ring|].
-    intros; apply Hvar; zify; omega.
-  + intros; apply Hvar; zify; omega.
+    intros; apply Hvar; lia.
+  + intros; apply Hvar; lia.
 Qed.
 
 End Evaluation.
@@ -424,7 +424,7 @@ match goal with
   apply Pos.max_case_strong; intros; lia
 | [ |- (?z < Pos.max ?x ?y)%positive ] =>
   apply Pos.max_case_strong; intros; lia
-| _ => zify; omega
+| _ => lia
 end : core.
 Hint Resolve Pos.le_max_r Pos.le_max_l : core.
 
@@ -488,7 +488,7 @@ induction Hl; intros kr pr Hr; simpl.
     { apply (valid_le_compat (Pos.max i kr)); auto. }
     { apply poly_add_valid_compat; auto.
       now apply poly_mul_mon_valid_compat; intuition. }
-  - repeat apply Pos.max_case_strong; zify; omega.
+  - repeat apply Pos.max_case_strong; lia.
 Qed.
 
 (* Compatibility of linearity wrt to linear operations *)
@@ -497,7 +497,7 @@ Lemma poly_add_linear_compat : forall kl kr pl pr, linear kl pl -> linear kr pr
   linear (Pos.max kl kr) (poly_add pl pr).
 Proof.
 intros kl kr pl pr Hl; revert kr pr; induction Hl; intros kr pr Hr; simpl.
-+ apply (linear_le_compat kr); [|apply Pos.max_case_strong; zify; omega].
++ apply (linear_le_compat kr); [|apply Pos.max_case_strong; lia].
   now induction Hr; constructor; auto.
 + apply (linear_le_compat (Pos.max kr (Pos.succ i))); [|now auto].
   induction Hr; simpl.
@@ -527,17 +527,17 @@ inversion Hv; case_decide; subst.
   destruct (list_nth k var false); ring_simplify; [|now auto].
   rewrite <- (andb_true_l (eval var p1)), <- (andb_true_l (eval var p3)).
   rewrite <- IHp2; auto; rewrite <- IHp1; [ring|].
-  apply (valid_le_compat k); [now auto|zify; omega].
+  apply (valid_le_compat k); [now auto|lia].
 + remember (list_nth k var false) as b; destruct b; ring_simplify; [|now auto].
   case_decide; simpl.
   - rewrite <- (IHp2 p2); [inversion H|now auto]; simpl.
     replace (eval var p1) with (list_nth k var false && eval var p1) by (rewrite <- Heqb; ring); rewrite <- (IHp1 k).
     { rewrite <- Heqb; ring. }
-    { apply (valid_le_compat p2); [auto|zify; omega]. }
+    { apply (valid_le_compat p2); [auto|lia]. }
   - rewrite (IHp2 p2); [|now auto].
     replace (eval var p1) with (list_nth k var false && eval var p1) by (rewrite <- Heqb; ring).
     rewrite <- (IHp1 k); [rewrite <- Heqb; ring|].
-    apply (valid_le_compat p2); [auto|zify; omega].
+    apply (valid_le_compat p2); [auto|lia].
 Qed.
 
 (* Reduction preserves evaluation by boolean assignations *)
@@ -555,10 +555,10 @@ Lemma reduce_aux_le_compat : forall k l p, valid k p -> (k <= l)%positive ->
   reduce_aux l p = reduce_aux k p.
 Proof.
 intros k l p; revert k l; induction p; intros k l H Hle; simpl; auto.
-inversion H; subst; repeat case_decide; subst; try (exfalso; zify; omega).
-+ apply IHp1; [|now auto]; eapply valid_le_compat; [eauto|zify; omega].
+inversion H; subst; repeat case_decide; subst; try lia.
++ apply IHp1; [|now auto]; eapply valid_le_compat; [eauto|lia].
 + f_equal; apply IHp1; auto.
-  now eapply valid_le_compat; [eauto|zify; omega].
+  now eapply valid_le_compat; [eauto|lia].
 Qed.
 
 (* Reduce projects valid polynomials into linear ones *)
@@ -569,13 +569,13 @@ intros i p; revert i; induction p; intros i Hp; simpl.
 + constructor.
 + inversion Hp; subst; case_decide; subst.
   - rewrite <- (Pos.max_id i) at 1; apply poly_add_linear_compat.
-    { apply IHp1; eapply valid_le_compat; [eassumption|zify; omega]. }
+    { apply IHp1; eapply valid_le_compat; [eassumption|lia]. }
     { intuition. }
   - case_decide.
-  { apply IHp1; eapply valid_le_compat; [eauto|zify; omega]. }
-  { constructor; try (zify; omega); auto.
-    erewrite (reduce_aux_le_compat p2); [|assumption|zify; omega].
-    apply IHp1; eapply valid_le_compat; [eauto|]; zify; omega. }
+  { apply IHp1; eapply valid_le_compat; [eauto|lia]. }
+  { constructor; try lia; auto.
+    erewrite (reduce_aux_le_compat p2); [|assumption|lia].
+    apply IHp1; eapply valid_le_compat; [eauto|]; lia. }
 Qed.
 
 Lemma linear_reduce : forall k p, valid k p -> linear k (reduce p).
@@ -583,7 +583,7 @@ Proof.
 intros k p H; induction H; simpl.
 + now constructor.
 + case_decide.
-  - eapply linear_le_compat; [eauto|zify; omega].
+  - eapply linear_le_compat; [eauto|lia].
   - constructor; auto.
     apply linear_reduce_aux; auto.
 Qed.
diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v
index 98f5ab067a..867fe69550 100644
--- a/plugins/btauto/Reflect.v
+++ b/plugins/btauto/Reflect.v
@@ -1,4 +1,4 @@
-Require Import Bool DecidableClass Algebra Ring PArith Omega.
+Require Import Bool DecidableClass Algebra Ring PArith Lia.
 
 Section Bool.
 
@@ -80,7 +80,7 @@ Qed.
 Hint Extern 5 => change 0 with (min 0 0) : core.
 Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat : core.
 Local Hint Constructors valid : core.
-Hint Extern 5 => zify; omega : core.
+Hint Extern 5 => lia : core.
 
 (* Compatibility with validity *)
 
@@ -203,7 +203,7 @@ intros A n; induction n using Pos.peano_rect; intros i x def Hd;
 + unfold make_last; rewrite Pos.peano_rect_succ; fold (make_last n x def).
   induction i using Pos.peano_case.
   - rewrite list_nth_base; reflexivity.
-  - rewrite list_nth_succ; apply IHn; zify; omega.
+  - rewrite list_nth_succ; apply IHn; lia.
 Qed.
 
 Lemma make_last_nth_2 : forall A n x def, list_nth n (@make_last A n x def) def = x.
@@ -226,7 +226,7 @@ intros var; induction var; intros i j x Hd; simpl.
   - rewrite Pos.peano_rect_succ.
     induction i using Pos.peano_rect.
     { rewrite 2list_nth_base; reflexivity. }
-    { rewrite 2list_nth_succ; apply IHvar; zify; omega. }
+    { rewrite 2list_nth_succ; apply IHvar; lia. }
 Qed.
 
 Lemma list_replace_nth_2 : forall var i x, list_nth i (list_replace var i x) false = x.
@@ -251,10 +251,10 @@ intros k p Hl Hp; induction Hl; simpl.
       assert (Hrw : b = true); [|rewrite Hrw; reflexivity]
     end.
     erewrite eval_suffix_compat; [now eauto| |now apply linear_valid_incl; eauto].
-    now intros j Hd; apply list_replace_nth_1; zify; omega.
+    now intros j Hd; apply list_replace_nth_1; lia.
     rewrite list_replace_nth_2, xorb_false_r.
     erewrite eval_suffix_compat; [now eauto| |now apply linear_valid_incl; eauto].
-    now intros j Hd; apply list_replace_nth_1; zify; omega.
+    now intros j Hd; apply list_replace_nth_1; lia.
 Qed.
 
 (* This should be better when using the [vm_compute] tactic instead of plain reflexivity. *)
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 :=
diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index 58d01c125c..896ee303cc 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -31,6 +31,7 @@ Require Export Ncring_tac.
 Require Export Integral_domain.
 Require Import DiscrR.
 Require Import ZArith.
+Require Import Lia.
 
 Declare ML Module "nsatz_plugin".
 
@@ -413,7 +414,7 @@ Ltac nsatz_generic radicalmax info lparam lvar :=
             try exact integral_domain_minus_one_zero
           || (solve [simpl; unfold R2, equality, eq_notation, addition, add_notation,
                      one, one_notation, multiplication, mul_notation, zero, zero_notation;
-                     discrR || omega]) 
+                     discrR || lia ])
           || ((*simpl*) idtac) || idtac "could not prove discrimination result"
         ]
       ]
@@ -502,7 +503,7 @@ reflexivity. exact Qplus_opp_r.
 Defined.
 
 Lemma Q_one_zero: not (Qeq 1%Q 0%Q).
-unfold Qeq. simpl. auto with *. Qed.
+Proof. unfold Qeq. simpl. lia.  Qed.
 
 Instance Qcri: (Cring (Rr:=Qri)).
 red. exact Qmult_comm. Defined.
@@ -513,8 +514,7 @@ exact Qmult_integral. exact Q_one_zero. Defined.
 
 (* Integers *)
 Lemma Z_one_zero: 1%Z <> 0%Z.
-omega. 
-Qed.
+Proof. lia. Qed.
 
 Instance Zcri: (Cring (Rr:=Zr)).
 red. exact Z.mul_comm. Defined.
diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v
index a0901202f7..8a51bcea02 100644
--- a/plugins/setoid_ring/Rings_Z.v
+++ b/plugins/setoid_ring/Rings_Z.v
@@ -17,8 +17,7 @@ Instance Zcri: (Cring (Rr:=Zr)).
 red. exact Z.mul_comm. Defined.
 
 Lemma Z_one_zero: 1%Z <> 0%Z.
-omega. 
-Qed.
+Proof. discriminate. Qed.
 
 Instance Zdi : (Integral_domain (Rcr:=Zcri)). 
 constructor. 
diff --git a/test-suite/bugs/closed/bug_2083.v b/test-suite/bugs/closed/bug_2083.v
index f33e96cea6..40fda71e66 100644
--- a/test-suite/bugs/closed/bug_2083.v
+++ b/test-suite/bugs/closed/bug_2083.v
@@ -13,15 +13,15 @@ Program Fixpoint check_n  (n : nat) (P : { i | i < n } -> bool) (p : nat)
         error
   end.
 
-Require Import Omega.
+Require Import Lia.
 
-Solve Obligations with program_simpl ; auto with *; try omega.
+Solve Obligations with program_simpl ; auto with *; lia.
 
 Next Obligation.
-  apply H. simpl. omega.
+  apply H. simpl. lia.
 Defined.
 
 Next Obligation.
-  case (le_lt_dec p i) ; intros. assert(i = p) by omega. subst.
+  case (le_lt_dec p i) ; intros. assert(i = p) by lia. subst.
   revert H0. clear_subset_proofs. auto.
   apply H. simpl. assumption. Defined.
diff --git a/test-suite/bugs/closed/bug_3652.v b/test-suite/bugs/closed/bug_3652.v
index 915cfcac27..b21a4d939c 100644
--- a/test-suite/bugs/closed/bug_3652.v
+++ b/test-suite/bugs/closed/bug_3652.v
@@ -1,6 +1,7 @@
 Require Setoid.
 Require ZArith.
 Import ZArith.
+Require Import Lia.
 
 Inductive Erasable(A : Set) : Prop :=
   erasable: A -> Erasable A.
@@ -87,12 +88,12 @@ Proof.
     unfold zotval.
     unfold mp2a1s.
     ring_simplify'.
-    replace 2 with (2*1) at 2 7 by omega.
+    replace 2 with (2*1) at 2 7 by lia.
     rewrite <-?Z.mul_assoc.
     rewrite <-?Z.mul_add_distr_l.
     rewrite <-Z.mul_sub_distr_l.
-    rewrite Z.mul_cancel_l by omega.
-    replace 1 with (2-1) at 1 by omega.
+    rewrite Z.mul_cancel_l by lia.
+    replace 1 with (2-1) at 1 by lia.
     rewrite Z.add_sub_assoc.
     rewrite Z.sub_cancel_r.
     Unshelve.
diff --git a/test-suite/bugs/closed/bug_4280.v b/test-suite/bugs/closed/bug_4280.v
index fd7897509e..31524e5dcf 100644
--- a/test-suite/bugs/closed/bug_4280.v
+++ b/test-suite/bugs/closed/bug_4280.v
@@ -1,11 +1,11 @@
-Require Import ZArith.
+Require Import ZArith Lia.
 Require Import Eqdep_dec.
 Local Open Scope Z_scope.
 
 Definition t := { n: Z | n > 1 }.
 
 Program Definition two : t := 2.
-Next Obligation. omega. Qed.
+Next Obligation. lia. Qed.
 
 Program Definition t_eq (x y: t) : {x=y} + {x<>y} :=
   if Z.eq_dec (proj1_sig x) (proj1_sig y) then left _ else right _.
diff --git a/test-suite/bugs/closed/bug_4306.v b/test-suite/bugs/closed/bug_4306.v
index f1bce04451..1ad84f9bb5 100644
--- a/test-suite/bugs/closed/bug_4306.v
+++ b/test-suite/bugs/closed/bug_4306.v
@@ -1,7 +1,7 @@
 Require Import List.
 Require Import Arith.
 Require Import Recdef.
-Require Import Omega.
+Require Import Lia.
 
 Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
   match xys with
@@ -14,9 +14,7 @@ Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys)
                               end
   end.
 Proof.
-  intros; simpl; omega.
-  intros; simpl; omega.
-  intros; simpl; omega.
+  all: simpl; lia.
 Qed.
 
 Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
diff --git a/test-suite/bugs/closed/bug_4456.v b/test-suite/bugs/closed/bug_4456.v
index 7685552725..0c26d4de32 100644
--- a/test-suite/bugs/closed/bug_4456.v
+++ b/test-suite/bugs/closed/bug_4456.v
@@ -10,7 +10,7 @@ Tactic Notation "admit" := case proof_admitted.
 
 Require Coq.Program.Program.
 Require Coq.Strings.String.
-Require Coq.omega.Omega.
+Require Coq.micromega.Lia.
 Module Export Fiat_DOT_Common.
 Module Export Fiat.
 Module Common.
@@ -489,7 +489,8 @@ Defined.
   End app.
 
 Import Coq.Lists.List.
-Import Coq.omega.Omega.
+Import Coq.Arith.Arith.
+Import Coq.micromega.Lia.
 Import Fiat_DOT_Common.Fiat.Common.
 Import Fiat.Parsers.ContextFreeGrammar.Valid.
 Local Open Scope string_like_scope.
@@ -585,8 +586,8 @@ Defined.
               | _ => discriminate
               | [ H : forall x, (_ * _)%type -> _ |- _ ] => specialize (fun x y z => H x (y, z))
               | _ => solve [ eauto with nocore ]
-              | _ => solve [ apply Min.min_case_strong; omega ]
-              | _ => omega
+              | _ => solve [ apply Min.min_case_strong; lia ]
+              | _ => lia
               | [ H : production_valid (_::_) |- _ ]
                 => let H' := fresh in
                    pose proof H as H';
diff --git a/test-suite/bugs/closed/bug_4852.v b/test-suite/bugs/closed/bug_4852.v
index e2e00f05d3..cdc8cd8b20 100644
--- a/test-suite/bugs/closed/bug_4852.v
+++ b/test-suite/bugs/closed/bug_4852.v
@@ -2,7 +2,7 @@
 
 Require Import Coq.Lists.List.
 Import ListNotations.
-Require Import Omega.
+Require Import Lia.
 
 Definition wfi_lt := well_founded_induction_type Wf_nat.lt_wf.
 
@@ -16,7 +16,7 @@ Tactic Notation "wfinduction" constr(term) "on" ne_hyp_list(Hs) "as" ident(H) :=
 
 Hint Rewrite @app_comm_cons @app_assoc @app_length : app_rws.
 
-Ltac solve_nat := autorewrite with app_rws in *; cbn in *; omega.
+Ltac solve_nat := autorewrite with app_rws in *; cbn in *; lia.
 
 Notation "| x |" := (length x) (at level 11, no associativity, format "'|' x '|'").
 
diff --git a/test-suite/bugs/opened/bug_1596.v b/test-suite/bugs/opened/bug_1596.v
index 27cb731151..89410047b2 100644
--- a/test-suite/bugs/opened/bug_1596.v
+++ b/test-suite/bugs/opened/bug_1596.v
@@ -1,7 +1,7 @@
 Require Import Relations.
 Require Import FSets.
 Require Import Arith.
-Require Import Omega.
+Require Import Lia.
 
 Set Keyed Unification.
 
@@ -147,14 +147,14 @@ Module MessageSpi.
     Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z).
       unfold lt.
       induction x;destruct y;simpl;try tauto;destruct z;try tauto;intros.
-      omega.
+      lia.
     Qed.
 
     Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y).
       unfold eq;unfold lt.
       induction x;destruct y;simpl;try tauto;intro;red;intro;try (discriminate
 H0);injection H0;intros.
-      elim (lt_irrefl n);try omega.
+      elim (lt_irrefl n); lia.
     Qed.
 
     Definition compare : forall (x y:t),(Compare lt eq x y).
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index 61ae4edbd1..398528de72 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -16,7 +16,7 @@ Check
     end
   in f 0.
 
-Require Import ZArith_base Omega.
+Require Import ZArith_base Lia.
 Open Scope Z_scope.
 
 Inductive even: Z -> Prop :=
@@ -35,13 +35,13 @@ Proof.
 fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
  intros.
  destruct H.
-   omega.
+   lia.
    apply odd_pos_even_pos in H.
-   omega.
+   lia.
  intros.
  destruct H.
   apply even_pos_odd_pos in H.
-  omega.
+  lia.
 Qed.
 
 CoInductive Inf := S { projS : Inf }.
diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v
index e777f10411..303acf7ae2 100644
--- a/theories/MSets/MSetEqProperties.v
+++ b/theories/MSets/MSetEqProperties.v
@@ -17,7 +17,7 @@
     [mem x s=true] instead of [In x s],
     [equal s s'=true] instead of [Equal s s'], etc. *)
 
-Require Import MSetProperties Zerob Sumbool Omega DecidableTypeEx.
+Require Import MSetProperties Zerob Sumbool Lia DecidableTypeEx.
 
 Module WEqPropertiesOn (Import E:DecidableType)(M:WSetsOn E).
 Module Import MP := WPropertiesOn E M.
@@ -845,19 +845,19 @@ unfold sum.
 intros f g Hf Hg.
 assert (fc : compat_opL (fun x:elt =>plus (f x))) by
  (repeat red; intros; rewrite Hf; auto).
-assert (ft : transposeL (fun x:elt =>plus (f x))) by (red; intros; omega).
+assert (ft : transposeL (fun x:elt =>plus (f x))) by (red; intros; lia).
 assert (gc : compat_opL (fun x:elt => plus (g x))) by
  (repeat red; intros; rewrite Hg; auto).
-assert (gt : transposeL (fun x:elt =>plus (g x))) by (red; intros; omega).
+assert (gt : transposeL (fun x:elt =>plus (g x))) by (red; intros; lia).
 assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))) by
   (repeat red; intros; rewrite Hf,Hg; auto).
-assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))) by (red; intros; omega).
+assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))) by (red; intros; lia).
 intros s;pattern s; apply set_rec.
 intros.
 rewrite <- (fold_equal _ _ _ _ fc ft 0 _ _ H).
 rewrite <- (fold_equal _ _ _ _ gc gt 0 _ _ H).
 rewrite <- (fold_equal _ _ _ _ fgc fgt 0 _ _ H); auto.
-intros. do 3 (rewrite fold_add; auto with *).
+intros. do 3 (rewrite fold_add; auto with fset). lia.
 do 3 rewrite fold_empty;auto.
 Qed.
 
@@ -869,7 +869,7 @@ assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).
 assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))) by
  (repeat red; intros; rewrite Hf; auto).
 assert (ct : transposeL (fun x => plus (if f x then 1 else 0))) by
- (red; intros; omega).
+ (red; intros; lia).
 intros s;pattern s; apply set_rec.
 intros.
 change elt with E.t.
@@ -919,7 +919,7 @@ Lemma sum_compat :
   forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s.
 intros.
 unfold sum; apply (@fold_compat _ (@Logic.eq nat));
- repeat red; auto with *.
+ repeat red; auto with *; lia.
 Qed.
 
 End Sum.
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. *)
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 90c82b677b..234063f14f 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import Omega Relations Multiset SetoidList.
+Require Import Lia Relations Multiset SetoidList.
 
 (** This file is deprecated, use [Permutation.v] instead.
 
@@ -189,7 +189,7 @@ Lemma permut_conv_inv :
   forall e l1 l2, permutation (e :: l1) (e :: l2) -> permutation l1 l2.
 Proof.
   intros e l1 l2; unfold permutation, meq; simpl; intros H a;
-    generalize (H a); apply plus_reg_l.
+    generalize (H a); lia.
 Qed.
 
 Lemma permut_app_inv1 :
@@ -199,9 +199,7 @@ Proof.
     intros H a; generalize (H a); clear H.
   do 2 rewrite list_contents_app.
   simpl.
-  intros; apply plus_reg_l with (multiplicity (list_contents l) a).
-  rewrite plus_comm; rewrite H; rewrite plus_comm.
-  trivial.
+  lia.
 Qed.
 
 (** we can use [multiplicity] to define [InA] and [NoDupA]. *)
@@ -220,8 +218,7 @@ Proof.
     intros H a; generalize (H a); clear H.
   do 2 rewrite list_contents_app.
   simpl.
-  intros; apply plus_reg_l with (multiplicity (list_contents l) a).
-  trivial.
+  lia.
 Qed.
 
 Lemma permut_remove_hd_eq :
@@ -230,13 +227,9 @@ Lemma permut_remove_hd_eq :
 Proof.
   unfold permutation, meq; simpl; intros l l1 l2 a b Heq H a0.
   specialize H with a0.
-  rewrite list_contents_app in *; simpl in *.
-  apply plus_reg_l with (if eqA_dec a a0 then 1 else 0).
-  rewrite H; clear H.
-  symmetry; rewrite plus_comm, <- ! plus_assoc; f_equal.
-  rewrite plus_comm.
-  destruct (eqA_dec a a0) as [Ha|Ha]; rewrite Heq in Ha;
-    decide (eqA_dec b a0) with Ha; reflexivity.
+  rewrite list_contents_app in *. simpl in *.
+  destruct (eqA_dec a _) as [Ha|Ha]; rewrite Heq in Ha; revert H;
+    decide (eqA_dec b a0) with Ha; lia.
 Qed.
 
 Lemma permut_remove_hd :
@@ -342,9 +335,9 @@ Proof.
   rewrite multiplicity_InA.
   specialize (H a).
   rewrite if_eqA_refl in H.
-  clear IHl; omega.
+  clear IHl; lia.
   rewrite IHl; intros.
-  specialize (H a0). omega.
+  specialize (H a0). lia.
 Qed.
 
 (** Permutation is compatible with InA. *)
@@ -395,14 +388,14 @@ Proof.
   apply permut_length_1.
   red; red; intros.
   specialize (P a). simpl in *.
-  rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto. omega.
+  rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto. lia.
   right.
   inversion_clear H0; [|inversion H].
   split; auto.
   apply permut_length_1.
   red; red; intros.
   specialize (P a); simpl in *.
-  rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto. omega.
+  rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto. lia.
 Qed.
 
 (** Permutation is compatible with length. *)
@@ -434,7 +427,7 @@ Proof.
   rewrite multiplicity_NoDupA in H, H0.
   generalize (H a) (H0 a) (H1 a); clear H H0 H1.
   do 2 rewrite multiplicity_InA.
-  destruct 3; omega.
+  destruct 3; lia.
 Qed.
 
 End Permut.