Merge PR #13741: Remove omega tactic (deprecated in 8.12)

Reviewed-by: Zimmi48
Ack-by: JasonGross
Ack-by: silene
Ack-by: SkySkimmer
Ack-by: olaure01

20 files changed, 109 insertions, 154 deletions

diff --git a/test-suite/bugs/closed/bug_1362.v b/test-suite/bugs/closed/bug_1362.v
index 6cafb9f0cd..18b8d743b3 100644
--- a/test-suite/bugs/closed/bug_1362.v
+++ b/test-suite/bugs/closed/bug_1362.v
@@ -1,26 +1,17 @@
 (** Omega is now aware of the bodies of context variables
     (of type Z or nat). *)
 
-Require Import ZArith Omega.
+Require Import ZArith Lia.
 Open Scope Z.
 
 Goal let x := 3 in x = 3.
 intros.
-omega.
+lia.
 Qed.
 
 Open Scope nat.
 
 Goal let x := 2 in x = 2.
 intros.
-omega.
+lia.
 Qed.
-
-(** NB: this could be disabled for compatibility reasons *)
-
-Unset Omega UseLocalDefs.
-
-Goal let x := 4 in x = 4.
-intros.
-Fail omega.
-Abort.
diff --git a/test-suite/bugs/closed/bug_1912.v b/test-suite/bugs/closed/bug_1912.v
index 0228abbb9b..9f6c8177f6 100644
--- a/test-suite/bugs/closed/bug_1912.v
+++ b/test-suite/bugs/closed/bug_1912.v
@@ -1,6 +1,6 @@
-Require Import Omega.
+Require Import Lia ZArith.
 
 Goal forall x, Z.succ (Z.pred x) = x.
 intros x.
-omega.
+lia.
 Qed.
diff --git a/test-suite/bugs/closed/bug_4132.v b/test-suite/bugs/closed/bug_4132.v
index 67ecc3087f..2ebbb66758 100644
--- a/test-suite/bugs/closed/bug_4132.v
+++ b/test-suite/bugs/closed/bug_4132.v
@@ -1,5 +1,5 @@
 
-Require Import ZArith Omega.
+Require Import ZArith Lia.
 Open Scope Z_scope.
 
 (** bug 4132: omega was using "simpl" either on whole equations, or on
@@ -14,18 +14,18 @@ Lemma foo
   (H : - zxy' <= zxy)
   (H' : zxy' <= x') : - b <= zxy.
 Proof.
-omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *)
+lia. (* was: Uncaught exception Invalid_argument("index out of bounds"). *)
 Qed.
 
 Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b.
-omega. (* Pierre L: according to a comment of bug report #4132,
+lia. (* Pierre L: according to a comment of bug report #4132,
           this might have triggered "index out of bounds" in the past,
           but I never managed to reproduce that in any version,
           even before my fix. *)
 Qed.
 
 Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b.
-omega. (* Pierre L: according to a comment of bug report #4132,
+lia. (* Pierre L: according to a comment of bug report #4132,
           this might have triggered "Failure(occurrence 2)" in the past,
           but I never managed to reproduce that. *)
 Qed.
diff --git a/test-suite/bugs/closed/bug_4717.v b/test-suite/bugs/closed/bug_4717.v
index bd9bac37ef..81bc70d076 100644
--- a/test-suite/bugs/closed/bug_4717.v
+++ b/test-suite/bugs/closed/bug_4717.v
@@ -1,6 +1,6 @@
 (* Omega being smarter on recognizing nat and Z *)
 
-Require Import Omega.
+Require Import Lia ZArith.
 
 Definition nat' := nat.
 
@@ -10,13 +10,13 @@ Theorem le_not_eq_lt : forall (n m:nat),
     n < m.
 Proof.
   intros.
-  omega.
+  lia.
 Qed.
 
 Goal forall (x n : nat'), x = x + n - n.
 Proof.
   intros.
-  omega.
+  lia.
 Qed.
 
 Open Scope Z_scope.
@@ -29,5 +29,5 @@ Theorem Zle_not_eq_lt : forall n m,
     n < m.
 Proof.
   intros.
-  omega.
+  lia.
 Qed.
diff --git a/test-suite/bugs/closed/bug_9512.v b/test-suite/bugs/closed/bug_9512.v
index bad9d64f65..f42e32cf25 100644
--- a/test-suite/bugs/closed/bug_9512.v
+++ b/test-suite/bugs/closed/bug_9512.v
@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt Coq.omega.Omega Coq.micromega.Lia.
+Require Import Coq.ZArith.BinInt Coq.micromega.Lia.
 
 Set Primitive Projections.
 Record params := { width : Z }.
@@ -10,7 +10,6 @@ Set Printing All.
 Lemma foo : width p = 0%Z -> width p = 0%Z.
   intros.
 
-  assert_succeeds (enough True; [omega|]).
   assert_succeeds (enough True; [lia|]).
 
 (*   H : @eq Z (width p) Z0 *)
@@ -26,12 +25,6 @@ Lemma foo : width p = 0%Z -> width p = 0%Z.
 (*   @eq Z (width p) Z0 *)
 
   assert_succeeds (enough True; [lia|]).
-  (* Tactic failure: <tactic closure> fails. *)
-  (* assert_succeeds (enough True; [omega|]). *)
-  (* Tactic failure: <tactic closure> fails. *)
-
-  (* omega. *)
-  (* Error: Omega can't solve this system *)
 
   lia.
   (* Tactic failure:  Cannot find witness. *)
diff --git a/test-suite/bugs/opened/bug_1615.v b/test-suite/bugs/opened/bug_1615.v
deleted file mode 100644
index c045335410..0000000000
--- a/test-suite/bugs/opened/bug_1615.v
+++ /dev/null
@@ -1,11 +0,0 @@
-Require Import Omega.
-
-Lemma foo : forall n m : Z, (n >= 0)%Z -> (n * m >= 0)%Z -> (n <= n + n * m)%Z.
-Proof.
-  intros. omega.
-Qed.
-
-Lemma foo' : forall n m : nat, n <=  n + n * m.
-Proof.
-  intros. Fail omega.
-Abort.
diff --git a/test-suite/bugs/opened/bug_6602.v b/test-suite/bugs/opened/bug_6602.v
deleted file mode 100644
index 3690adf90a..0000000000
--- a/test-suite/bugs/opened/bug_6602.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Omega.
-
-Lemma test_nat:
-  forall n, (5 + pred n <= 5 + n).
-Proof.
-  intros.
-  zify.
-  omega.
-Qed.
-
-Lemma test_N:
-  forall n, (5 + N.pred n <= 5 + n)%N.
-Proof.
-  intros.
-  zify.
-  omega.
-Qed.
diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v
index d2e6794c0b..1f4913b49d 100644
--- a/test-suite/interactive/ParalITP_smallproofs.v
+++ b/test-suite/interactive/ParalITP_smallproofs.v
@@ -140,35 +140,35 @@ Qed.
 Lemma lt_minus_neq : forall m n : nat, m < n -> n - m <> 0.
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 Lemma lt_minus_eq_0 : forall m n : nat, m < n -> m - n = 0.
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 Lemma le_plus_Sn_1_SSn : forall n : nat, S n + 1 <= S (S n).
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 Lemma le_plus_O_l : forall p q : nat, p + q <= 0 -> p = 0.
 Proof. 
- intros; omega.
+ intros; lia.
 Qed.
 
 Lemma le_plus_O_r : forall p q : nat, p + q <= 0 -> q = 0.
 Proof. 
- intros; omega.
+ intros; lia.
 Qed.
 
 Lemma minus_pred : forall m n : nat, 0 < n -> pred m - pred n = m - n.
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 
@@ -1414,13 +1414,13 @@ Qed.
 Lemma lt_inj : forall m n : nat, (m < n)%Z -> m < n.
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 Lemma le_inj : forall m n : nat, (m <= n)%Z -> m <= n.
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 
@@ -1501,7 +1501,7 @@ Proof.
   [ replace (Zabs_nat x) with (Zabs_nat (x - 1 + 1));
      [ idtac | apply f_equal with Z; auto with zarith ];
      rewrite absolu_plus;
-     [ unfold Zabs_nat at 2, nat_of_P, Piter_op in |- *; omega
+     [ unfold Zabs_nat at 2, nat_of_P, Piter_op in |- *; lia
      | auto with zarith
      | intro; discriminate ]
   | rewrite <- H1; reflexivity ].
diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
index 69ed621877..ae71ddfd1d 100644
--- a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
+++ b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
@@ -19,6 +19,7 @@
 
 Require Export ZArith.
 Require Export ZArithRing.
+Require Import Lia.
 
 Tactic Notation "ElimCompare" constr(c) constr(d) := elim_compare c d.
 
@@ -140,35 +141,35 @@ Qed.
 Lemma lt_minus_neq : forall m n : nat, m < n -> n - m <> 0.
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 Lemma lt_minus_eq_0 : forall m n : nat, m < n -> m - n = 0.
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 Lemma le_plus_Sn_1_SSn : forall n : nat, S n + 1 <= S (S n).
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 Lemma le_plus_O_l : forall p q : nat, p + q <= 0 -> p = 0.
 Proof.
- intros; omega.
+ intros; lia.
 Qed.
 
 Lemma le_plus_O_r : forall p q : nat, p + q <= 0 -> q = 0.
 Proof.
- intros; omega.
+ intros; lia.
 Qed.
 
 Lemma minus_pred : forall m n : nat, 0 < n -> pred m - pred n = m - n.
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 
@@ -573,7 +574,7 @@ Qed.
 
 
 
-Hint Resolve Zmult_pos_pos Zmult_neg_neg Zmult_neg_pos Zmult_pos_neg: zarith.
+Local Hint Resolve Zmult_pos_pos Zmult_neg_neg Zmult_neg_pos Zmult_pos_neg: zarith.
 
 
 Lemma Zle_reg_mult_l :
@@ -1158,7 +1159,7 @@ Proof.
  intros [| p| p]; intros; [ Falsum | constructor | constructor ].
 Qed.
 
-Hint Resolve square_pos: zarith.
+Local Hint Resolve square_pos: zarith.
 
 (*###########################################################################*)
 (** Properties of positive numbers, mapping between Z and nat                *)
@@ -1414,13 +1415,13 @@ Qed.
 Lemma lt_inj : forall m n : nat, (m < n)%Z -> m < n.
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 Lemma le_inj : forall m n : nat, (m <= n)%Z -> m <= n.
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 
@@ -1501,7 +1502,7 @@ Proof.
   [ replace (Z.abs_nat x) with (Z.abs_nat (x - 1 + 1));
      [ idtac | apply f_equal with Z; auto with zarith ];
      rewrite absolu_plus;
-     [ unfold Z.abs_nat at 2, nat_of_P, Pos.iter_op in |- *; omega
+     [ unfold Z.abs_nat at 2, nat_of_P, Pos.iter_op in |- *; lia
      | auto with zarith
      | intro; discriminate ]
   | rewrite <- H1; reflexivity ].
@@ -1985,7 +1986,7 @@ Proof.
  intros [| p| p] Hp; trivial.
 Qed.
 
-Hint Resolve Zsgn_1 Zsgn_2 Zsgn_3 Zsgn_4 Zsgn_5 Zsgn_6 Zsgn_7 Zsgn_7' Zsgn_8
+Local Hint Resolve Zsgn_1 Zsgn_2 Zsgn_3 Zsgn_4 Zsgn_5 Zsgn_6 Zsgn_7 Zsgn_7' Zsgn_8
   Zsgn_9 Zsgn_10 Zsgn_11 Zsgn_12 Zsgn_13 Zsgn_14 Zsgn_15 Zsgn_16 Zsgn_17
   Zsgn_18 Zsgn_19 Zsgn_20 Zsgn_21 Zsgn_22 Zsgn_23 Zsgn_24 Zsgn_25 Zsgn_26
   Zsgn_27: zarith.
@@ -2388,7 +2389,7 @@ Proof.
  intros [|z|z]; simpl; auto with zarith; apply Zle_neg_pos.
 Qed.
 
-Hint Resolve Zabs_1 Zabs_2 Zabs_3 Zabs_4 Zabs_5 Zabs_6 Zabs_7 Zabs_8 Zabs_9
+Local Hint Resolve Zabs_1 Zabs_2 Zabs_3 Zabs_4 Zabs_5 Zabs_6 Zabs_7 Zabs_8 Zabs_9
   Zabs_10 Zabs_11 Zabs_12 Zabs_min Zabs_neg Zabs_mult Zabs_plus Zle_Zabs: zarith.
 
 
@@ -2949,7 +2950,7 @@ Proof.
  ring.
 Qed.
 
-Hint Resolve ZmaxSS Zle_max_r Zle_max_l Zmax_n_n: zarith.
+Local Hint Resolve ZmaxSS Zle_max_r Zle_max_l Zmax_n_n: zarith.
 
 (*###########################################################################*)
 (** Properties of Arity                                                      *)
@@ -3020,7 +3021,7 @@ Proof.
  Flip.
 Qed.
 
-Hint Resolve Z_div_mod_eq_2 Z_div_le Z_div_nonneg Z_div_neg: zarith.
+Local Hint Resolve Z_div_mod_eq_2 Z_div_le Z_div_nonneg Z_div_neg: zarith.
 
 (*###########################################################################*)
 (** Properties of Zpower                                                       *)
@@ -3038,4 +3039,4 @@ Proof.
   ring.
 Qed.
 
-Hint Resolve Zpower_1 Zpower_2: zarith.
+Local Hint Resolve Zpower_1 Zpower_2: zarith.
diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v
index d52a853aae..24634bd321 100644
--- a/test-suite/success/Abstract.v
+++ b/test-suite/success/Abstract.v
@@ -1,6 +1,6 @@
 (* Cf BZ#546 *)
 
-Require Import Omega.
+Require Import Lia.
 
 Section S.
 
@@ -19,7 +19,7 @@ induction n.
  replace (2 * S n0) with (2*n0 + 2) ; auto with arith.
   apply DummyApp.
    2:exact Dummy2.
-   apply IHn0 ; abstract omega.
+   apply IHn0 ; abstract lia.
 Defined.
 
 End S.
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v
index 5e0f90d59b..bbdf9762a3 100644
--- a/test-suite/success/Omega.v
+++ b/test-suite/success/Omega.v
@@ -1,5 +1,5 @@
 
-Require Import Omega.
+Require Import Lia ZArith.
 
 (* Submitted by Xavier Urbain 18 Jan 2002 *)
 
@@ -7,14 +7,14 @@ Lemma lem1 :
  forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z.
 Proof.
 intros x y.
- omega.
+ lia.
 Qed.
 
 (* Proposed by Pierre Crégut *)
 
 Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z.
 intro.
- omega.
+ lia.
 Qed.
 
 (* Proposed by Jean-Christophe Filliâtre *)
@@ -22,7 +22,7 @@ Qed.
 Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z.
 Proof.
 intros.
- omega.
+ lia.
 Qed.
 
 (* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
@@ -32,7 +32,7 @@ Section A.
 Variable x y : Z.
 Hypothesis H : (x > y)%Z.
 Lemma lem4 : (x > y)%Z.
- omega.
+ lia.
 Qed.
 End A.
 
@@ -48,7 +48,7 @@ Hypothesis L : (R1 >= 0)%Z -> S2 = S1.
 Hypothesis M : (H <= 2 * S)%Z.
 Hypothesis N : (S < H)%Z.
 Lemma lem5 : (H > 0)%Z.
- omega.
+ lia.
 Qed.
 End B.
 
@@ -56,11 +56,11 @@ End B.
 Lemma lem6 :
  forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z.
 intros.
- omega.
+ lia.
 Qed.
 
 (* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *)
-Require Import Omega.
+Require Import Lia.
 Section C.
 Parameter g : forall m : nat, m <> 0 -> Prop.
 Parameter f : forall (m : nat) (H : m <> 0), g m H.
@@ -68,21 +68,21 @@ Variable n : nat.
 Variable ap_n : n <> 0.
 Let delta := f n ap_n.
 Lemma lem7 : n = n.
- omega.
+ lia.
 Qed.
 End C.
 
 (* Problem of dependencies *)
-Require Import Omega.
+Require Import Lia.
 Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0.
-intros;  omega.
+intros;  lia.
 Qed.
 
 (* Bug that what caused by the use of intro_using in Omega *)
-Require Import Omega.
+Require Import Lia.
 Lemma lem9 :
  forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p.
-intros;  omega.
+intros;  lia.
 Qed.
 
 (* Check that the interpretation of mult on nat enforces its positivity *)
@@ -90,5 +90,5 @@ Qed.
 (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *)
 Lemma lem10 : forall n m:nat, le n (plus n (mult n m)).
 Proof.
-intros; zify; omega.
+intros; lia.
 Qed.
diff --git a/test-suite/success/Omega0.v b/test-suite/success/Omega0.v
index 6fd936935c..6ce7264b7a 100644
--- a/test-suite/success/Omega0.v
+++ b/test-suite/success/Omega0.v
@@ -1,4 +1,4 @@
-Require Import ZArith Omega.
+Require Import ZArith Lia.
 Open Scope Z_scope.
 
 (* Pierre L: examples gathered while debugging romega. *)
@@ -8,7 +8,7 @@ Lemma test_romega_0 :
   0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
 Proof.
 intros.
-omega.
+lia.
 Qed.
 
 Lemma test_romega_0b :
@@ -16,7 +16,7 @@ Lemma test_romega_0b :
   0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
 Proof.
 intros m m'.
-omega.
+lia.
 Qed.
 
 Lemma test_romega_1 :
@@ -29,7 +29,7 @@ Lemma test_romega_1 :
     z >= 0.
 Proof.
 intros.
-omega.
+lia.
 Qed.
 
 Lemma test_romega_1b :
@@ -42,21 +42,21 @@ Lemma test_romega_1b :
     z >= 0.
 Proof.
 intros z z1 z2.
-omega.
+lia.
 Qed.
 
 Lemma test_romega_2 : forall a b c:Z,
  0<=a-b<=1 -> b-c<=2 -> a-c<=3.
 Proof.
 intros.
-omega.
+lia.
 Qed.
 
 Lemma test_romega_2b : forall a b c:Z,
  0<=a-b<=1 -> b-c<=2 -> a-c<=3.
 Proof.
 intros a b c.
-omega.
+lia.
 Qed.
 
 Lemma test_romega_3 : forall a b h hl hr ha hb,
@@ -70,7 +70,7 @@ Lemma test_romega_3 : forall a b h hl hr ha hb,
  0 <= hb - h <= 1.
 Proof.
 intros.
-omega.
+lia.
 Qed.
 
 Lemma test_romega_3b : forall a b h hl hr ha hb,
@@ -84,7 +84,7 @@ Lemma test_romega_3b : forall a b h hl hr ha hb,
  0 <= hb - h <= 1.
 Proof.
 intros a b h hl hr ha hb.
-omega.
+lia.
 Qed.
 
 
@@ -94,7 +94,7 @@ Lemma test_romega_4 : forall hr ha,
  hr = 0.
 Proof.
 intros hr ha.
-omega.
+lia.
 Qed.
 
 Lemma test_romega_5 : forall hr ha,
@@ -103,45 +103,45 @@ Lemma test_romega_5 : forall hr ha,
  hr = 0.
 Proof.
 intros hr ha.
-omega.
+lia.
 Qed.
 
 Lemma test_romega_6 : forall z, z>=0 -> 0>z+2 -> False.
 Proof.
 intros.
-omega.
+lia.
 Qed.
 
 Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False.
 Proof.
 intros z.
-omega.
+lia.
 Qed.
 
 Lemma test_romega_7 : forall z,
   0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
 Proof.
 intros.
-omega.
+lia.
 Qed.
 
 Lemma test_romega_7b : forall z,
   0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
 Proof.
 intros.
-omega.
+lia.
 Qed.
 
 (* Magaud BZ#240 *)
 
 Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
 intros.
-omega.
+lia.
 Qed.
 
 Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
 intros x y.
-omega.
+lia.
 Qed.
 
 
diff --git a/test-suite/success/Omega2.v b/test-suite/success/Omega2.v
index 4e726335c9..b2eef5bcd5 100644
--- a/test-suite/success/Omega2.v
+++ b/test-suite/success/Omega2.v
@@ -1,4 +1,4 @@
-Require Import ZArith Omega.
+Require Import ZArith Lia.
 
 (* Submitted by Yegor Bryukhov (BZ#922) *)
 
@@ -23,6 +23,6 @@ forall v1 v2 v3 v4 v5 : Z,
 ((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9))
 -> False.
 intros.
-omega.
+lia.
 Qed.
 
diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v
index 0223255067..32bc99621a 100644
--- a/test-suite/success/OmegaPre.v
+++ b/test-suite/success/OmegaPre.v
@@ -1,4 +1,4 @@
-Require Import ZArith Nnat Omega.
+Require Import ZArith Nnat Lia.
 Open Scope Z_scope.
 
 (** Test of the zify preprocessor for (R)Omega *)
@@ -16,112 +16,111 @@ Open Scope Z_scope.
 
 Goal forall a:Z, Z.max a a = a.
 intros.
-zify; omega.
+lia.
 Qed.
 
 Goal forall a b:Z, Z.max a b = Z.max b a.
 intros.
-zify; omega.
+lia.
 Qed.
 
 Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c.
 intros.
-zify; omega.
+lia.
 Qed.
 
 Goal forall a b:Z, Z.max a b + Z.min a b = a + b.
 intros.
-zify; omega.
+lia.
 Qed.
 
 Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a.
 intros.
-zify.
-intuition; subst; zify; omega. (* pure multiplication: zify; omega alone can't do it *)
+intuition; subst; lia.
 Qed.
 
 Goal forall a:Z, Z.abs a = a -> a >= 0.
 intros.
-zify; omega.
+lia.
 Qed.
 
 Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1.
 intros.
-zify; omega.
+lia.
 Qed.
 
 (* zify_nat *)
 
 Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat.
 intros.
-zify; omega.
+lia.
 Qed.
 
 Goal forall m:nat, (m<1)%nat -> (m=0)%nat.
 intros.
-zify; omega.
+lia.
 Qed.
 
 Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat.
 intros.
-zify; omega.
+lia.
 Qed.
 (* 2000 instead of 200: works, but quite slow *)
 
 Goal forall m: nat, (m*m>=0)%nat.
 intros.
-zify; omega.
+lia.
 Qed.
 
 (* zify_positive *)
 
 Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive.
 intros.
-zify; omega.
+lia.
 Qed.
 
 Goal forall m:positive, (m<2)%positive -> (m=1)%positive.
 intros.
-zify; omega.
+lia.
 Qed.
 
 Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive.
 intros.
-zify; omega.
+lia.
 Qed.
 
 Goal forall m: positive, (m*m>=1)%positive.
 intros.
-zify; omega.
+lia.
 Qed.
 
 (* zify_N *)
 
 Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N.
 intros.
-zify; omega.
+lia.
 Qed.
 
 Goal forall m:N, (m<1)%N -> (m=0)%N.
 intros.
-zify; omega.
+lia.
 Qed.
 
 Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N.
 intros.
-zify; omega.
+lia.
 Qed.
 
 Goal forall m:N, (m*m>=0)%N.
 intros.
-zify; omega.
+lia.
 Qed.
 
 (* mix of datatypes *)
 
 Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p.
 intros.
-zify; omega.
+lia.
 Qed.
 
 
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index 02adb012d9..ef8617cd9e 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -85,19 +85,19 @@ Time Program Fixpoint check_n  (n : nat) (P : { i | i < n } -> bool) (p : nat)
         error
   end.
 
-Require Import Omega Setoid.
+Require Import Lia Setoid.
 
 Next Obligation.
   intros ; simpl in *. apply H.
-  simpl in * ; omega.
+  simpl in * ; lia.
 Qed.
 
 Next Obligation. simpl in *; intros.
   revert H0 ; clear_subset_proofs. intros.
-  case (le_gt_dec p i) ; intro. simpl in *. assert(p = i) by omega. subst.
+  case (le_gt_dec p i) ; intro. simpl in *. assert(p = i) by lia. subst.
   revert H0 ; clear_subset_proofs ; tauto.
 
-  apply H. simpl. omega.
+  apply H. simpl. lia.
 Qed.
 
 Program Fixpoint check_n'  (n : nat) (m : {m:nat | m = n}) (p : nat) (q:{q : nat | q = p})
diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v
index 6ca32f450f..c0e86b00dd 100644
--- a/test-suite/success/ROmegaPre.v
+++ b/test-suite/success/ROmegaPre.v
@@ -32,8 +32,7 @@ Qed.
 
 Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a.
 intros.
-zify.
-intuition; subst; lia. (* pure multiplication: omega alone can't do it *)
+intuition; subst; lia.
 Qed.
 
 Goal forall a:Z, Z.abs a = a -> a >= 0.
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index ff34840d83..b7d5276bc8 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.v
@@ -61,7 +61,7 @@ Qed.
 
 (* Check mutually inductive statements *)
 
-Require Import ZArith_base Omega.
+Require Import ZArith_base Lia.
 Open Scope Z_scope.
 
 Inductive even: Z -> Prop :=
@@ -75,13 +75,13 @@ with odd_pos_even_pos : forall n, odd n -> n >= 1.
 Proof.
  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 a : Prop := acons : b -> a
diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v
index 5638a7d3eb..06847f4f96 100644
--- a/test-suite/success/keyedrewrite.v
+++ b/test-suite/success/keyedrewrite.v
@@ -23,7 +23,7 @@ Qed.
 Print Equivalent Keys.
 End foo.
 
-Require Import Arith List Omega.
+Require Import Arith List.
 
 Definition G {A} (f : A -> A -> A) (x : A) := f x x.
 
diff --git a/test-suite/success/rewrite_iterated.v b/test-suite/success/rewrite_iterated.v
index 962dada35a..946011e393 100644
--- a/test-suite/success/rewrite_iterated.v
+++ b/test-suite/success/rewrite_iterated.v
@@ -1,8 +1,8 @@
-Require Import Arith Omega.
+Require Import Arith Lia.
 
 Lemma test : forall p:nat, p<>0 -> p-1+1=p.
 Proof.
- intros; omega.
+ intros; lia.
 Qed.
 
 (** Test of new syntax for rewrite : ! ? and so on... *)
diff --git a/test-suite/success/search.v b/test-suite/success/search.v
index 92de43e052..627e109d5f 100644
--- a/test-suite/success/search.v
+++ b/test-suite/success/search.v
@@ -32,4 +32,4 @@ Require Import ZArith.
 
 Search Z.mul Z.add "distr".
 Search "+"%Z "*"%Z "distr" -positive -Prop.
-Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
+Search (?x * _ + ?x * _)%Z outside Lia.