Merge PR #10937: [stdlib]Reals: use “lia” rather than “omega”

Reviewed-by: ppedrot

16 files changed, 130 insertions, 132 deletions

diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index d09b3248ef..b411c4953a 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -14,7 +14,7 @@ Require Import SeqSeries.
 Require Import Rtrigo_def.
 Require Import Cos_rel.
 Require Import Max.
-Require Import Omega.
+Require Import Lia.
 Local Open Scope nat_scope.
 Local Open Scope R_scope.
 
@@ -213,7 +213,7 @@ Proof.
   apply le_n_S.
   apply plus_le_compat_l; assumption.
   rewrite pred_of_minus.
-  omega.
+  lia.
   apply Rle_trans with
     (sum_f_R0
       (fun k:nat =>
@@ -236,7 +236,7 @@ Proof.
   apply Rmult_le_compat_l.
   left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
   apply C_maj.
-  omega.
+  lia.
   right.
   unfold Rdiv; rewrite Rmult_comm.
   unfold Binomial.C.
@@ -248,7 +248,7 @@ Proof.
   unfold Rsqr; reflexivity.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
-  omega.
+  lia.
   apply INR_fact_neq_0.
   unfold Rdiv; rewrite Rmult_comm.
   unfold Binomial.C.
@@ -258,7 +258,7 @@ Proof.
   replace (2 * S (N + n) - 2 * S (n0 + n))%nat with (2 * (N - n0))%nat.
   rewrite mult_INR.
   reflexivity.
-  omega.
+  lia.
   apply INR_fact_neq_0.
   apply Rle_trans with
     (sum_f_R0 (fun k:nat => INR N / INR (fact (S N)) * C ^ (4 * N)) (pred N)).
@@ -279,7 +279,7 @@ Proof.
   apply Rmult_le_compat_l.
   apply Rle_0_sqr.
   apply le_INR.
-  omega.
+  lia.
   rewrite Rmult_comm; unfold Rdiv; apply Rmult_le_compat_l.
   apply pos_INR.
   apply Rle_trans with (/ INR (fact (S (N + n)))).
@@ -458,7 +458,7 @@ Proof.
     (2 * (N - n0) + 1 + (2 * S (n0 + n) + 1))%nat.
   repeat rewrite pow_add.
   ring.
-  omega.
+  lia.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   apply Rle_ge; left; apply Rinv_0_lt_compat.
@@ -517,7 +517,7 @@ Proof.
   replace (2 * S (S (n0 + n)))%nat with (S (2 * S (n0 + n) + 1)).
   apply le_n_Sn.
   ring.
-  omega.
+  lia.
   right.
   unfold Rdiv; rewrite Rmult_comm.
   unfold Binomial.C.
@@ -529,7 +529,7 @@ Proof.
   unfold Rsqr; reflexivity.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
-  omega.
+  lia.
   apply INR_fact_neq_0.
   unfold Rdiv; rewrite Rmult_comm.
   unfold Binomial.C.
@@ -540,7 +540,7 @@ Proof.
     (2 * (N - n0) + 1)%nat.
   rewrite mult_INR.
   reflexivity.
-  omega.
+  lia.
   apply INR_fact_neq_0.
   apply Rle_trans with
     (sum_f_R0 (fun k:nat => INR N / INR (fact (S (S N))) * C ^ (4 * S N))
@@ -563,8 +563,8 @@ Proof.
   apply Rle_0_sqr.
   replace (S (pred (N - n))) with (N - n)%nat.
   apply le_INR.
-  omega.
-  omega.
+  lia.
+  lia.
   rewrite Rmult_comm; unfold Rdiv; apply Rmult_le_compat_l.
   apply pos_INR.
   apply Rle_trans with (/ INR (fact (S (S (N + n))))).
@@ -592,7 +592,7 @@ Proof.
   rewrite Rmult_1_r.
   apply le_INR.
   apply fact_le.
-  omega.
+  lia.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   rewrite sum_cte.
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index d5086db6cf..4ce5cd6b1c 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -12,7 +12,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
 Require Import Rtrigo_def.
-Require Import OmegaTactic.
+Require Import Lia.
 Local Open Scope R_scope.
 
 Definition A1 (x:R) (N:nat) : R :=
@@ -149,13 +149,13 @@ unfold Wn.
 apply Rmult_eq_compat_l.
 replace (2 * S i - S (2 * i0))%nat with (S (2 * (i - i0))).
 reflexivity.
-omega.
+lia.
 apply sum_eq; intros.
 unfold Wn.
 apply Rmult_eq_compat_l.
 replace (2 * S i - 2 * i0)%nat with (2 * (S i - i0))%nat.
 reflexivity.
-omega.
+lia.
 replace
  (-
   sum_f_R0
@@ -211,7 +211,7 @@ replace (S (2 * i0)) with (2 * i0 + 1)%nat;
  [ apply Rmult_eq_compat_l | ring ].
 replace (2 * S i - (2 * i0 + 1))%nat with (2 * (i - i0) + 1)%nat.
 reflexivity.
-omega.
+lia.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
@@ -240,7 +240,7 @@ rewrite Rmult_1_l.
 rewrite Rinv_mult_distr.
 replace (2 * i - 2 * i0)%nat with (2 * (i - i0))%nat.
 reflexivity.
-omega.
+lia.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index 9205df1bb7..2ae93c8705 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 Require Import RIneq.
-Require Import Omega.
+Require Import Lia.
 Local Open Scope R_scope.
 
 Lemma Rlt_R0_R2 : 0 < 2.
@@ -49,7 +49,7 @@ Ltac omega_sup :=
   repeat
     rewrite <- plus_IZR ||
       rewrite <- mult_IZR || rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus;
-  apply IZR_lt; omega.
+  apply IZR_lt; lia.
 
 Ltac prove_sup :=
   match goal with
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 1636d81d25..2c822da055 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -17,7 +17,7 @@ Require Import PSeries_reg.
 Require Import Div2.
 Require Import Even.
 Require Import Max.
-Require Import Omega.
+Require Import Lia.
 Local Open Scope nat_scope.
 Local Open Scope R_scope.
 
@@ -488,8 +488,8 @@ Proof.
   rewrite div2_S_double.
   apply S_pred with 0%nat; apply H3.
   reflexivity.
-  omega.
-  omega.
+  lia.
+  lia.
   rewrite H2.
   replace (pred (S (2 * N0))) with (2 * N0)%nat; [ idtac | reflexivity ].
   replace (S (S (2 * N0))) with (2 * S N0)%nat.
@@ -549,15 +549,15 @@ Proof.
   rewrite H6.
   replace (pred (2 * N1)) with (S (2 * pred N1)).
   rewrite div2_S_double.
-  omega.
-  omega.
+  lia.
+  lia.
   assert (0 < n)%nat.
   apply lt_le_trans with 2%nat.
   apply lt_O_Sn.
   apply le_trans with (max (2 * S N0) 2).
   apply le_max_r.
   apply H3.
-  omega.
+  lia.
   rewrite H6.
   replace (pred (S (2 * N1))) with (2 * N1)%nat.
   rewrite div2_double.
diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v
index 08bc38a085..d5a39f527f 100644
--- a/theories/Reals/Machin.v
+++ b/theories/Reals/Machin.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import Omega.
+Require Import Lia.
 Require Import Lra.
 Require Import Rbase.
 Require Import Rtrigo1.
@@ -163,8 +163,8 @@ assert (cv : Un_cv PI_2_3_7_tg 0).
   rewrite <- (Rmult_0_r 2), <- Ropp_mult_distr_r_reverse.
   rewrite <- Rmult_plus_distr_l, Rabs_mult, (Rabs_pos_eq 2);[|lra].
   rewrite Rmult_assoc; apply Rmult_lt_compat_l;[lra | ].
-   apply (Pn1 n); omega.
-  apply (Pn2 n); omega.
+   apply (Pn1 n); lia.
+  apply (Pn2 n); lia.
 rewrite Machin_2_3_7.
 rewrite !atan_eq_ps_atan; try (split; lra).
 unfold ps_atan; destruct (in_int (/3)); destruct (in_int (/7));
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 7813c7b975..229e6018ca 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -19,7 +19,7 @@ Require Export Raxioms.
 Require Import Rpow_def.
 Require Import Zpower.
 Require Export ZArithRing.
-Require Import Omega.
+Require Import Lia.
 Require Export RealField.
 
 Local Open Scope Z_scope.
@@ -1875,7 +1875,7 @@ Lemma eq_IZR : forall n m:Z, IZR n = IZR m -> n = m.
 Proof.
   intros z1 z2 H; generalize (Rminus_diag_eq (IZR z1) (IZR z2) H);
     rewrite (Z_R_minus z1 z2); intro; generalize (eq_IZR_R0 (z1 - z2) H0);
-      intro; omega.
+      intro; lia.
 Qed.
 
 (**********)
@@ -1913,21 +1913,21 @@ Qed.
 Lemma IZR_ge : forall n m:Z, (n >= m)%Z -> IZR n >= IZR m.
 Proof.
   intros m n H; apply Rnot_lt_ge; red; intro.
-  generalize (lt_IZR m n H0); intro; omega.
+  generalize (lt_IZR m n H0); intro; lia.
 Qed.
 
 Lemma IZR_le : forall n m:Z, (n <= m)%Z -> IZR n <= IZR m.
 Proof.
   intros m n H; apply Rnot_gt_le; red; intro.
-  unfold Rgt in H0; generalize (lt_IZR n m H0); intro; omega.
+  unfold Rgt in H0; generalize (lt_IZR n m H0); intro; lia.
 Qed.
 
 Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m.
 Proof.
   intros m n H; cut (m <= n)%Z.
   intro H0; elim (IZR_le m n H0); intro; auto.
-  generalize (eq_IZR m n H1); intro; exfalso; omega.
-  omega.
+  generalize (eq_IZR m n H1); intro; exfalso; lia.
+  lia.
 Qed.
 
 Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 <> IZR z2.
@@ -1954,7 +1954,7 @@ Lemma one_IZR_r_R1 :
   forall r (n m:Z), r < IZR n <= r + 1 -> r < IZR m <= r + 1 -> n = m.
 Proof.
   intros r z x [H1 H2] [H3 H4].
-  cut ((z - x)%Z = 0%Z); auto with zarith.
+  cut ((z - x)%Z = 0%Z). lia.
   apply one_IZR_lt1.
   rewrite <- Z_R_minus; split.
   replace (-1) with (r - (r + 1)).
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index 5365e04000..5f0747d869 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -14,7 +14,7 @@
 (**********************************************************)
 
 Require Import Rbase.
-Require Import Omega.
+Require Import Lia.
 Local Open Scope R_scope.
 
 (*********************************************************)
@@ -60,7 +60,7 @@ Proof.
   apply lt_IZR in H1.
   rewrite <- minus_IZR in H2.
   apply le_IZR in H2.
-  omega.
+  lia.
 Qed.
 
 (**********)
@@ -230,7 +230,7 @@ Proof.
     rewrite <- (plus_IZR (Int_part r1 - Int_part r2) 1) in H;
       generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2) H0 H);
         intros; clear H H0; unfold Int_part at 1;
-          omega.
+          lia.
 Qed.
 
 (**********)
@@ -314,7 +314,7 @@ Proof.
                                                                                                               in H0; fold (IZR (Int_part r1) - IZR (Int_part r2) - 1) in H0;
                                                                                                                 rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0;
                                                                                                                   rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H;
-                                                                                                                    auto with zarith real.
+                                                                                                                    auto with real.
   change (_ + -1) with (IZR (Int_part r1 - Int_part r2) - 1) in H;
     rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H;
       rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H0;
@@ -323,7 +323,7 @@ Proof.
             intro; clear H;
               generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2 - 1) H1 H0);
                 intros; clear H0 H1; unfold Int_part at 1;
-                  omega.
+                  lia.
 Qed.
 
 (**********)
@@ -430,14 +430,14 @@ Proof.
                                                                     clear a b;
                                                                       change 2 with (1 + 1) in H0;
                                                                       rewrite <- (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2)) 1 1) in H0;
-                                                                        auto with zarith real.
+                                                                        auto with real.
     rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H;
       rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0;
         rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H;
           rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H0;
             rewrite <- (plus_IZR (Int_part r1 + Int_part r2 + 1) 1) in H0;
               generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2 + 1) H H0);
-                intro; clear H H0; unfold Int_part at 1; omega.
+                intro; clear H H0; unfold Int_part at 1; lia.
 Qed.
 
 (**********)
@@ -499,7 +499,7 @@ Proof.
         rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1;
           generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2) H0 H1);
             intro; clear H0 H1; unfold Int_part at 1;
-              omega.
+              lia.
 Qed.
 
 (**********)
@@ -522,7 +522,7 @@ Proof.
                         rewrite
                           (Rplus_assoc (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))) (-(1)))
                           ; rewrite <- (Ropp_plus_distr (IZR (Int_part r1) + IZR (Int_part r2)) 1);
-                            trivial with zarith real.
+                            trivial with real.
 Qed.
 
 (**********)
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index 7a838f2772..3f560f202e 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -11,7 +11,6 @@
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis1.
-Require Import Omega.
 Local Open Scope R_scope.
 
 (**********)
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index ca82222c25..11835bd24a 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -16,7 +16,7 @@ Require Import Lra.
 Require Import RiemannInt.
 Require Import SeqProp.
 Require Import Max.
-Require Import Omega.
+Require Import Lia.
 Require Import Lra.
 Local Open Scope R_scope.
 
@@ -1095,11 +1095,11 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn
    apply Rlt_trans with (Rabs h * eps / 4 + Rabs (f x - fn N x) + Rabs h * Rabs (fn' N c - g x)).
     apply Rplus_lt_compat_r ; apply Rplus_lt_compat_r ; unfold R_dist in fnxh_CV_fxh ;
  rewrite Rabs_minus_sym ; apply fnxh_CV_fxh.
-   unfold N; omega.
+   unfold N; lia.
    apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * Rabs (fn' N c - g x)).
     apply Rplus_lt_compat_r ; apply Rplus_lt_compat_l.
     unfold R_dist in fnx_CV_fx ; rewrite Rabs_minus_sym ; apply fnx_CV_fx.
-    unfold N ; omega.
+    unfold N ; lia.
    replace (fn' N c - g x)  with ((fn' N c - g c) +  (g c - g x)) by field.
    apply Rle_lt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 +
           Rabs h * Rabs (fn' N c - g c) + Rabs h * Rabs (g c - g x)).
@@ -1113,7 +1113,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn
     apply Rplus_lt_compat_r; apply Rplus_lt_compat_l; apply Rmult_lt_compat_l.
      apply Rabs_pos_lt ; assumption.
     rewrite Rabs_minus_sym ; apply fn'c_CVU_gc.
-     unfold N ; omega.
+     unfold N ; lia.
     assert (t : Boule x delta c).
      destruct P.
      apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta.
@@ -1201,11 +1201,11 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn
    apply Rlt_trans with (Rabs h * eps / 4 + Rabs (f x - fn N x) + Rabs h * Rabs (fn' N c - g x)).
     apply Rplus_lt_compat_r ; apply Rplus_lt_compat_r ; unfold R_dist in fnxh_CV_fxh ;
  rewrite Rabs_minus_sym ; apply fnxh_CV_fxh.
-   unfold N; omega.
+   unfold N; lia.
    apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * Rabs (fn' N c - g x)).
     apply Rplus_lt_compat_r ; apply Rplus_lt_compat_l.
     unfold R_dist in fnx_CV_fx ; rewrite Rabs_minus_sym ; apply fnx_CV_fx.
-    unfold N ; omega.
+    unfold N ; lia.
    replace (fn' N c - g x)  with ((fn' N c - g c) +  (g c - g x)) by field.
    apply Rle_lt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 +
           Rabs h * Rabs (fn' N c - g c) + Rabs h * Rabs (g c - g x)).
@@ -1219,7 +1219,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn
     apply Rplus_lt_compat_r; apply Rplus_lt_compat_l; apply Rmult_lt_compat_l.
      apply Rabs_pos_lt ; assumption.
     rewrite Rabs_minus_sym ; apply fn'c_CVU_gc.
-     unfold N ; omega.
+     unfold N ; lia.
     assert (t : Boule x delta c).
      destruct P.
     apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta.
diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v
index 57bc89b7e5..e822b87cc6 100644
--- a/theories/Reals/Ratan.v
+++ b/theories/Reals/Ratan.v
@@ -20,7 +20,7 @@ Require Import SeqProp.
 Require Import Ranalysis5.
 Require Import SeqSeries.
 Require Import PartSum.
-Require Import Omega.
+Require Import Lia.
 
 Local Open Scope R_scope.
 
@@ -76,30 +76,30 @@ clear.
 intros [ | n] P Hs Ho;[solve[apply Ho, Hs] | apply Hs; auto with arith].
 intros N; pattern N; apply WLOG; clear N.
 intros [ | N] Npos n decr to0 cv nN.
-  clear -Npos; elimtype False; omega.
+  lia.
  assert (decr' : Un_decreasing (fun i => f (S N + i)%nat)).
   intros k; replace (S N+S k)%nat with (S (S N+k)) by ring.
   apply (decr (S N + k)%nat).
  assert (to' : Un_cv (fun i => f (S N + i)%nat) 0).
   intros eps ep; destruct (to0 eps ep) as [M PM].
-  exists M; intros k kM; apply PM; omega.
+  exists M; intros k kM; apply PM; lia.
  assert (cv' : Un_cv
          (sum_f_R0 (tg_alt (fun i => ((-1) ^ S N * f(S N + i)%nat))))
              (l - sum_f_R0 (tg_alt f) N)).
   intros eps ep; destruct (cv eps ep) as [M PM]; exists M.
   intros n' nM. 
   match goal with |- ?C => set (U := C) end.
-  assert (nM' : (n' + S N >= M)%nat) by omega.
+  assert (nM' : (n' + S N >= M)%nat) by lia.
    generalize (PM _ nM'); unfold R_dist.
   rewrite (tech2 (tg_alt f) N (n' + S N)).
   assert (t : forall a b c, (a + b) - c = b - (c - a)) by (intros; ring).
   rewrite t; clear t; unfold U, R_dist; clear U.
-  replace (n' + S N - S N)%nat with n' by omega.
+  replace (n' + S N - S N)%nat with n' by lia.
   rewrite <- (sum_eq (tg_alt (fun i => (-1) ^ S N * f(S N + i)%nat))).
    tauto.
    intros i _; unfold tg_alt.
    rewrite <- Rmult_assoc, <- pow_add, !(plus_comm i); reflexivity.
-  omega.
+  lia.
   assert (cv'' : Un_cv (sum_f_R0 (tg_alt (fun i => f (S N + i)%nat)))
                    ((-1) ^ S N * (l - sum_f_R0 (tg_alt f) N))).
   apply (Un_cv_ext (fun n => (-1) ^ S N * 
@@ -118,7 +118,7 @@ intros [ | N] Npos n decr to0 cv nN.
    rewrite neven.
    destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E].
    unfold R_dist; rewrite Rabs_pos_eq;[ | lra].
-   assert (dist : (p <= p')%nat) by omega.
+   assert (dist : (p <= p')%nat) by lia.
    assert (t := decreasing_prop _ _ _ (CV_ALT_step1 f decr) dist).
    apply Rle_trans with (sum_f_R0 (tg_alt f) (2 * p) - l).
     unfold Rminus; apply Rplus_le_compat_r; exact t.
@@ -129,7 +129,7 @@ intros [ | N] Npos n decr to0 cv nN.
   rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E].
    unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_minus_distr;
      [ | lra].
-   assert (dist : (p <= p')%nat) by omega.
+   assert (dist : (p <= p')%nat) by lia.
    apply Rle_trans with (l - sum_f_R0 (tg_alt f) (S (2 * p))).
     unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar.
     solve[apply Rge_le, (growing_prop _ _ _ (CV_ALT_step0 f decr) dist)].
@@ -142,11 +142,11 @@ intros [ | N] Npos n decr to0 cv nN.
    rewrite neven;
    destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E].
    unfold R_dist; rewrite Rabs_pos_eq;[ | lra].
-   assert (dist : (S p < S p')%nat) by omega.
+   assert (dist : (S p < S p')%nat) by lia.
    apply Rle_trans with (sum_f_R0 (tg_alt f) (2 * S p) - l).
    unfold Rminus; apply Rplus_le_compat_r,
      (decreasing_prop _ _ _ (CV_ALT_step1 f decr)).
-   omega.
+   lia.
   rewrite keep, tech5; unfold tg_alt at 2; rewrite <- keep, pow_1_even.
   lra.
  rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E].
@@ -154,7 +154,7 @@ intros [ | N] Npos n decr to0 cv nN.
  rewrite Ropp_minus_distr.
  apply Rle_trans with (l - sum_f_R0 (tg_alt f) (S (2 * p))).
   unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar, Rge_le,
-   (growing_prop _ _ _ (CV_ALT_step0 f decr)); omega.
+   (growing_prop _ _ _ (CV_ALT_step0 f decr)); lia.
  generalize C; rewrite keep, tech5; unfold tg_alt.
  rewrite <- keep, pow_1_even.
  assert (t : forall a b c, a <= b + 1 * c -> a - b <= c) by (intros; lra).
@@ -166,7 +166,7 @@ clear WLOG; intros Hyp [ | n] decr to0 cv _.
  intros [A B]; rewrite Rabs_pos_eq; lra.
 apply Rle_trans with (f 1%nat).
  apply (Hyp 1%nat (le_n 1) (S n) decr to0 cv).
- omega.
+ lia.
 solve[apply decr].
 Qed.
 
@@ -746,7 +746,7 @@ intros x Hx n.
  apply Rlt_le.
  apply Rinv_0_lt_compat.
  apply lt_INR_0.
- omega.
+ lia.
  destruct (proj1 Hx) as [Hx1|Hx1].
  destruct (proj2 Hx) as [Hx2|Hx2].
  (* . 0 < x < 1 *)
@@ -762,7 +762,7 @@ intros x Hx n.
  rewrite Rmult_1_r.
  exact Hx1.
  exact Hx2.
- omega.
+ lia.
  apply Rgt_not_eq.
  exact Hx1.
  (* . x = 1 *)
@@ -771,13 +771,13 @@ intros x Hx n.
  apply Rle_refl.
  (* . x = 0 *)
  rewrite <- Hx1.
- do 2 (rewrite pow_i ; [ idtac | omega ]).
+ do 2 (rewrite pow_i ; [ idtac | lia ]).
  apply Rle_refl.
  apply Rlt_le.
  apply Rinv_lt_contravar.
- apply Rmult_lt_0_compat ; apply lt_INR_0 ; omega.
+ apply Rmult_lt_0_compat ; apply lt_INR_0 ; lia.
  apply lt_INR.
- omega.
+ lia.
 Qed.
 
 Lemma Ratan_seq_converging : forall x, (0 <= x <= 1)%R -> Un_cv (Ratan_seq x) 0.
@@ -808,7 +808,7 @@ intros x Hx eps Heps.
    apply Rlt_le.
    apply Rinv_0_lt_compat.
    apply lt_INR_0.
-   omega.
+   lia.
    apply pow_incr.
    exact Hx.
    rewrite pow1.
@@ -817,15 +817,15 @@ intros x Hx eps Heps.
    rewrite Rmult_1_l.
    apply Rinv_le_contravar.
    apply lt_INR_0.
-   omega.
+   lia.
    apply le_INR.
-   omega.
+   lia.
    rewrite <- (Rinv_involutive eps).
    apply Rinv_lt_contravar.
    apply Rmult_lt_0_compat.
    auto with real.
    apply lt_INR_0.
-   omega.
+   lia.
    apply Rlt_trans with (INR N).
    destruct (archimed (/ eps)) as (H,_).
    assert (0 < up (/ eps))%Z.
@@ -837,7 +837,7 @@ intros x Hx eps Heps.
    rewrite INR_IZR_INZ, positive_nat_Z.
    exact HN.
    apply lt_INR.
-   omega.
+   lia.
    apply Rgt_not_eq.
    exact Heps.
    apply Rle_ge.
@@ -848,7 +848,7 @@ intros x Hx eps Heps.
    apply Rlt_le.
    apply Rinv_0_lt_compat.
    apply lt_INR_0.
-   omega.
+   lia.
 Qed.
 
 Definition ps_atan_exists_01 (x : R) (Hx:0 <= x <= 1) :
@@ -1045,7 +1045,7 @@ intros x n x_lb ; unfold Datan_seq ; induction n.
  apply Rmult_gt_0_compat.
  replace (x^2) with (x*x) by field ; apply Rmult_gt_0_compat ; assumption.
  assumption.
- replace (2 * S n)%nat with (S (S (2 * n))) by intuition.
+ replace (2 * S n)%nat with (S (S (2 * n))) by lia.
  simpl ; field.
 Qed.
 
@@ -1067,8 +1067,7 @@ Lemma Datan_seq_increasing : forall x y n, (n > 0)%nat -> 0 <= x < y -> Datan_se
 Proof.
 intros x y n n_lb x_encad ; assert (x_pos : x >= 0) by intuition.
  assert (y_pos : y > 0). apply Rle_lt_trans with (r2:=x) ; intuition.
- induction n.
- apply False_ind ; intuition.
+ induction n. lia.
  clear -x_encad x_pos y_pos ; induction n ; unfold Datan_seq.
  case x_pos ; clear x_pos ; intro x_pos.
  simpl ; apply Rmult_gt_0_lt_compat ; intuition. lra.
@@ -1077,14 +1076,14 @@ intros x y n n_lb x_encad ; assert (x_pos : x >= 0) by intuition.
  simpl ; field.
  intuition.
  assert (Hrew : forall a, a^(2 * S (S n)) = (a ^ 2) * (a ^ (2 * S n))).
-  clear ; intro a ; replace (2 * S (S n))%nat with (S (S (2 * S n)))%nat by intuition.
+  clear ; intro a ; replace (2 * S (S n))%nat with (S (S (2 * S n)))%nat by lia.
   simpl ; field.
  case x_pos ; clear x_pos ; intro x_pos.
  rewrite Hrew ; rewrite Hrew.
  apply Rmult_gt_0_lt_compat ; intuition.
  apply Rmult_gt_0_lt_compat ; intuition ; lra.
  rewrite x_pos.
- rewrite pow_i ; intuition.
+ rewrite pow_i. intuition. lia.
 Qed.
 
 Lemma Datan_seq_decreasing : forall x,  -1 < x -> x < 1 -> Un_decreasing (Datan_seq x).
@@ -1101,7 +1100,7 @@ assert (intabs : 0 <= Rabs x < 1).
  split;[apply Rabs_pos | apply Rabs_def1]; tauto.
 apply (pow_lt_1_compat (Rabs x) 2) in intabs.
  tauto.
-omega.
+lia.
 Qed.
 
 Lemma Datan_seq_CV_0 : forall x, -1 < x -> x < 1 -> Un_cv (Datan_seq x) 0.
@@ -1112,7 +1111,7 @@ assert (x_ub2 : Rabs (x^2) < 1).
  rewrite <- pow2_abs.
  assert (H: 0 <= Rabs x < 1)
    by (split;[apply Rabs_pos | apply Rabs_def1; auto]).
- apply (pow_lt_1_compat _ 2) in H;[tauto | omega].
+ apply (pow_lt_1_compat _ 2) in H;[tauto | lia].
 elim (pow_lt_1_zero (x^2) x_ub2 eps eps_pos) ; intros N HN ; exists N ; intros n Hn.
 unfold R_dist, Datan_seq.
 replace (x ^ (2 * n) - 0) with ((x ^ 2) ^ n). apply HN ; assumption.
@@ -1130,7 +1129,7 @@ assert (Tool2 : / (1 + x ^ 2) > 0).
  apply Rinv_0_lt_compat ; tauto.
 assert (x_ub2' : 0<= Rabs (x^2) < 1).
  rewrite Rabs_pos_eq, <- pow2_abs;[ | apply pow2_ge_0].
- apply pow_lt_1_compat;[split;[apply Rabs_pos | ] | omega].
+ apply pow_lt_1_compat;[split;[apply Rabs_pos | ] | lia].
  apply Rabs_def1; assumption.
 assert (x_ub2 : Rabs (x^2) < 1) by tauto.
 assert (eps'_pos : ((1+x^2)*eps) > 0).
@@ -1164,7 +1163,7 @@ assert (tool : forall a b c, 0 < b -> a < b * c -> a * / b < c).
   assumption.
  field; apply Rgt_not_eq; exact bp.
 apply tool;[exact Tool1 | ].
-apply HN; omega.
+apply HN; lia.
 Qed.
 
 Lemma Datan_CVU_prelim : forall c (r : posreal), Rabs c + r < 1 ->
@@ -1187,7 +1186,7 @@ apply (Alt_CVU (fun x n => Datan_seq n x)
   intros x [ | n] inb.
    solve[unfold Datan_seq; apply Rle_refl].
   rewrite <- (Datan_seq_Rabs x); apply Rlt_le, Datan_seq_increasing.
-   omega.
+   lia.
   apply Boule_lt in inb; intuition.
   solve[apply Rabs_pos].
  apply Datan_seq_CV_0.
@@ -1212,7 +1211,7 @@ assert (Tool : forall N, (-1) ^ (S (2 * N))  = - 1).
   rewrite <- pow_add.
   replace (2 + S (2 * n))%nat with (S (2 * S n))%nat.
   reflexivity.
-  intuition.
+  lia.
 intros N x x_lb x_ub.
  induction N.
   unfold Datan_seq, Ratan_seq, tg_alt ; simpl.
@@ -1251,10 +1250,10 @@ intros N x x_lb x_ub.
    apply Rabs_pos_lt ; assumption.
    rewrite Rabs_right.
    replace 1 with (/1) by field.
-   apply Rinv_1_lt_contravar ; intuition.
+   apply Rinv_1_lt_contravar. lra. apply lt_1_INR; lia.
    apply Rgt_ge ; replace (INR (2 * S N + 1)) with (INR (2*S N) + 1) ;
    [apply RiemannInt.RinvN_pos | ].
-   replace (2 * S N + 1)%nat with (S (2 * S N))%nat by intuition ;
+   replace (2 * S N + 1)%nat with (S (2 * S N))%nat by lia.
    rewrite S_INR ; reflexivity.
    apply Hdelta ; assumption.
    rewrite Rmult_minus_distr_l.
@@ -1266,7 +1265,7 @@ intros N x x_lb x_ub.
       - (x ^ (2 * S N + 1) / INR (2 * S N + 1))) / h)) by intuition.
    apply Rplus_eq_compat_l. field.
    split ; [apply Rgt_not_eq|] ; intuition.
-   clear ; replace (pred (2 * S N + 1)) with (2 * S N)%nat by intuition.
+   clear ; replace (pred (2 * S N + 1)) with (2 * S N)%nat by lia.
    field ; apply Rgt_not_eq ; intuition.
    field ; split ; [apply Rgt_not_eq |] ; intuition.
    elim (Main (eps/3) eps_3_pos) ; intros delta2 Hdelta2.
@@ -1314,7 +1313,7 @@ apply (Alt_CVU (fun i r => Ratan_seq r i) ps_atan PI_tg (/2) pos_half);
  intros x n b; apply Boule_half_to_interval in b.
  rewrite <- (Rmult_1_l (PI_tg n)); unfold Ratan_seq, PI_tg. 
  apply Rmult_le_compat_r.
-  apply Rlt_le, Rinv_0_lt_compat, (lt_INR 0); omega.
+  apply Rlt_le, Rinv_0_lt_compat, (lt_INR 0); lia.
  rewrite <- (pow1 (2 * n + 1)); apply pow_incr; assumption.
 exact PI_tg_cv.
 Qed.
@@ -1458,10 +1457,10 @@ rewrite Rplus_assoc ; apply Rabs_triang.
    apply Halpha ; split.
    unfold D_x, no_cond ; split ; [ | apply Rgt_not_eq ] ; intuition.
    intuition.
-   apply HN2; unfold N; omega.
+   apply HN2; unfold N; lia.
    lra.
   rewrite <- Rabs_Ropp, Ropp_minus_distr; apply HN1.
-     unfold N; omega.  
+     unfold N; lia.
     lra.
   assumption.
  field.
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index effbc3a404..69a41db4db 100644
--- a/theories/Reals/Rderiv.v
+++ b/theories/Reals/Rderiv.v
@@ -17,7 +17,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rlimit.
 Require Import Lra.
-Require Import Omega.
+Require Import Lia.
 Local Open Scope R_scope.
 
 (*********)
@@ -341,7 +341,7 @@ Proof.
   rewrite cond in H2; rewrite cond; simpl in H2; simpl;
     cut (1 + x0 * 1 * 0 = 1 * 1);
       [ intro A; rewrite A in H2; assumption | ring ].
-  cut (n0 <> 0%nat -> S (n0 - 1) = n0); [ intro | omega ];
+  cut (n0 <> 0%nat -> S (n0 - 1) = n0); [ intro | lia ];
     rewrite (H3 cond) in H2; rewrite (Rmult_comm (x0 ^ n0) (INR n0)) in H2;
       rewrite (tech_pow_Rplus x0 n0 n0) in H2; assumption.
 Qed.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 17b39d22cb..7f9e019c5b 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -25,7 +25,7 @@ Require Export R_sqr.
 Require Export SplitAbsolu.
 Require Export SplitRmult.
 Require Export ArithProp.
-Require Import Omega.
+Require Import Lia.
 Require Import Zpower.
 Local Open Scope nat_scope.
 Local Open Scope R_scope.
@@ -122,7 +122,7 @@ Hint Resolve pow_lt: real.
 Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n.
 Proof.
   intros x n; elim n; simpl; auto with real.
-  intros H' H'0; exfalso; omega.
+  intros H' H'0; exfalso; lia.
   intros n0; case n0.
   simpl; rewrite Rmult_1_r; auto.
   intros n1 H' H'0 H'1.
@@ -262,14 +262,14 @@ Proof.
   elim (IZN (up (b * / (Rabs x - 1))) H2); intros; exists x0;
     apply
       (Rge_trans (INR x0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))).
-  rewrite INR_IZR_INZ; apply IZR_ge; omega.
+  rewrite INR_IZR_INZ; apply IZR_ge; lia.
   unfold Rge; left; assumption.
   exists 0%nat;
     apply
       (Rge_trans (INR 0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))).
-  rewrite INR_IZR_INZ; apply IZR_ge; simpl; omega.
+  rewrite INR_IZR_INZ; apply IZR_ge; simpl; lia.
   unfold Rge; left; assumption.
-  omega.
+  lia.
 Qed.
 
 Lemma pow_ne_zero : forall n:nat, n <> 0%nat -> 0 ^ n = 0.
@@ -745,7 +745,7 @@ Proof.
   - now simpl; rewrite Rmult_1_l.
   - now rewrite <- !pow_powerRZ, Rpow_mult_distr.
   - destruct Hmxy as [H|H].
-    + assert(m = 0) as -> by now omega.
+    + assert(m = 0) as -> by now lia.
       now rewrite <- Hm, Rmult_1_l.
     + assert(x0 <> 0)%R by now intros ->; apply H; rewrite Rmult_0_l.
       assert(y0 <> 0)%R by now intros ->; apply H; rewrite Rmult_0_r.
@@ -808,7 +808,7 @@ Proof.
   ring.
   rewrite Rmult_plus_distr_r; rewrite Hrecn; cut ((n + 1)%nat = S n).
   intro H; rewrite H; simpl; ring.
-  omega.
+  lia.
 Qed.
 
 Lemma sum_f_R0_triangle :
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index 15ec7891f7..ed2c953449 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -14,7 +14,7 @@ Require Import Rfunctions.
 Require Import Rseries.
 Require Import PartSum.
 Require Import Binomial.
-Require Import Omega.
+Require Import Lia.
 Local Open Scope R_scope.
 
 (** TT Ak; 0<=k<=N *)
@@ -34,16 +34,16 @@ Lemma prod_SO_split :
     prod_f_R0 An k * prod_f_R0 (fun l:nat => An (k +1+l)%nat) (n - k -1).
 Proof.
   intros; induction  n as [| n Hrecn].
-  absurd (k < 0)%nat; omega.
-  cut (k = n \/ (k < n)%nat);[intro; elim H0; intro|omega].
-  replace (S n - k - 1)%nat with O; [rewrite H1; simpl|omega].
+  absurd (k < 0)%nat; lia.
+  cut (k = n \/ (k < n)%nat);[intro; elim H0; intro|lia].
+  replace (S n - k - 1)%nat with O; [rewrite H1; simpl|lia].
   replace (n+1+0)%nat with (S n); ring.
-  replace (S n - k-1)%nat with (S (n - k-1));[idtac|omega].
+  replace (S n - k-1)%nat with (S (n - k-1));[idtac|lia].
   simpl; replace (k + S (n - k))%nat with (S n).
   replace (k + 1 + S (n - k - 1))%nat with (S n).
   rewrite Hrecn; [ ring | assumption ].
-  omega.
-  omega.
+  lia.
+  lia.
 Qed.
 
 (**********)
@@ -116,11 +116,11 @@ Proof.
   assert (forall (n:nat), (0 < n)%nat ->
      (if eq_nat_dec n 0 then 1 else INR n) = INR n).
   intros n; case (eq_nat_dec n 0); auto with real.
-  intros; absurd (0 < n)%nat; omega.
+  intros; absurd (0 < n)%nat; lia.
   intros; unfold Rsqr; repeat rewrite fact_prodSO.
   cut ((k=N)%nat \/ (k < N)%nat \/ (N < k)%nat).
   intro H2; elim H2; intro H3.
-  rewrite H3; replace (2*N-N)%nat with N;[right; ring|omega].
+  rewrite H3; replace (2*N-N)%nat with N;[right; ring|lia].
   case H3; intro; clear H2 H3.
   rewrite (prod_SO_split (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) (2 * N - k) N).
   rewrite Rmult_assoc; apply Rmult_le_compat_l.
@@ -133,12 +133,12 @@ Proof.
   apply prod_SO_Rle; intros; split; auto.
   rewrite H0.
   rewrite H0.
-  apply le_INR; omega.
-  omega.
-  omega.
+  apply le_INR; lia.
+  lia.
+  lia.
   assumption.
-  omega.
-  omega.
+  lia.
+  lia.
   rewrite <- (Rmult_comm (prod_f_R0 (fun l:nat =>
           if eq_nat_dec l 0 then 1 else INR l) k));
     rewrite (prod_SO_split (fun l:nat =>
@@ -154,13 +154,13 @@ Proof.
   apply prod_SO_Rle; intros; split; auto.
   rewrite H0.
   rewrite H0.
-  apply le_INR; omega.
-  omega.
-  omega.
-  omega.
-  omega.
+  apply le_INR; lia.
+  lia.
+  lia.
+  lia.
+  lia.
   assumption.
-  omega.
+  lia.
 Qed.
 
 
@@ -192,5 +192,5 @@ Proof.
   reflexivity.
   rewrite mult_INR; apply prod_neq_R0; apply INR_fact_neq_0.
   apply prod_neq_R0; apply INR_fact_neq_0.
-  omega.
+  lia.
 Qed.
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index 2a9c6953c5..7577c4b7b0 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -12,7 +12,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
 Require Import PartSum.
-Require Import Omega.
+Require Import Lia.
 Local Open Scope R_scope.
 
 Set Implicit Arguments.
@@ -57,12 +57,12 @@ Section Sigma.
     ring.
     replace (high - S (S k))%nat with (high - S k - 1)%nat.
     apply pred_of_minus.
-    omega.
+    lia.
     unfold sigma; replace (S k - low)%nat with (S (k - low)).
     pattern (S k) at 1; replace (S k) with (low + S (k - low))%nat.
     symmetry ; apply (tech5 (fun i:nat => f (low + i))).
-    omega.
-    omega.
+    lia.
+    lia.
     rewrite <- H2; unfold sigma; rewrite <- minus_n_n; simpl;
       replace (high - S low)%nat with (pred (high - low)).
     replace (sum_f_R0 (fun k0:nat => f (S (low + k0))) (pred (high - low))) with
@@ -73,7 +73,7 @@ Section Sigma.
     apply sum_eq; intros; replace (S (low + i)) with (low + S i)%nat.
     reflexivity.
     ring.
-    omega.
+    lia.
     inversion H; [ right; reflexivity | left; assumption ].
   Qed.
 
diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v
index 0df1442f46..c2651d4120 100644
--- a/theories/Reals/Rtrigo1.v
+++ b/theories/Reals/Rtrigo1.v
@@ -18,7 +18,7 @@ Require Export Cos_rel.
 Require Export Cos_plus.
 Require Import ZArith_base.
 Require Import Zcomplements.
-Import Omega.
+Require Import Lia.
 Require Import Lra.
 Require Import Ranalysis1.
 Require Import Rsqrt_def. 
@@ -1741,7 +1741,7 @@ Proof.
       replace (3*(PI/2)) with (PI/2 + PI) in GT by field.
       rewrite Rplus_comm in GT.
       now apply Rplus_lt_reg_l in GT. }
-    omega.
+    lia.
 Qed.
 
 Lemma cos_eq_0_2PI_1 (x:R) :
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index d73f6ce0f3..34ea323a95 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -12,7 +12,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
 Require Import Max.
-Require Import Omega.
+Require Import Lia.
 Local Open Scope R_scope.
 
 (*****************************************************************)
@@ -1155,7 +1155,7 @@ Proof.
   rewrite Rmult_1_r; apply Rle_trans with (INR M_nat).
   left; rewrite INR_IZR_INZ.
   rewrite <- H4; assert (H8 := archimed (Rabs x)); elim H8; intros; assumption.
-  apply le_INR; omega.
+  apply le_INR; lia.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   ring.