Merge PR #8425: Deprecate romega in favor of lia

3 files changed, 24 insertions, 24 deletions

diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index 3452967821..c0db8646c7 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -27,7 +27,7 @@
 
 *)
 
-Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega.
+Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -39,7 +39,7 @@ Import Raw.Proofs.
 Local Open Scope pair_scope.
 Local Open Scope Int_scope.
 
-Ltac omega_max := i2z_refl; romega with Z.
+Ltac omega_max := i2z_refl; lia.
 
 Section Elt.
 Variable elt : Type.
@@ -697,7 +697,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   end.
   Proof.
   intros; unfold cardinal_e_2; simpl;
-  abstract (do 2 rewrite cons_cardinal_e; romega with * ).
+  abstract (do 2 rewrite cons_cardinal_e; lia ).
   Defined.
 
   Definition Cmp c :=
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index ec480bb1eb..4a1f24b95e 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -21,7 +21,7 @@ Require Import Znumtheory.
 Require Import Zgcd_alt.
 Require Import Zpow_facts.
 Require Import CyclicAxioms.
-Require Import ROmega.
+Require Import Lia.
 
 Local Open Scope nat_scope.
 Local Open Scope int31_scope.
@@ -1237,7 +1237,7 @@ Section Int31_Specs.
   destruct (Z_lt_le_dec (X+Y) wB).
   contradict H1; auto using Zmod_small with zarith.
   rewrite <- (Z_mod_plus_full (X+Y) (-1) wB).
-  rewrite Zmod_small; romega.
+  rewrite Zmod_small; lia.
 
  generalize (Z.compare_eq ((X+Y) mod wB) (X+Y)); intros Heq.
  destruct Z.compare; intros;
@@ -1261,7 +1261,7 @@ Section Int31_Specs.
   destruct (Z_lt_le_dec (X+Y+1) wB).
   contradict H1; auto using Zmod_small with zarith.
   rewrite <- (Z_mod_plus_full (X+Y+1) (-1) wB).
-  rewrite Zmod_small; romega.
+  rewrite Zmod_small; lia.
 
  generalize (Z.compare_eq ((X+Y+1) mod wB) (X+Y+1)); intros Heq.
  destruct Z.compare; intros;
@@ -1299,8 +1299,8 @@ Section Int31_Specs.
   unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros.
   destruct (Z_lt_le_dec (X-Y) 0).
   rewrite <- (Z_mod_plus_full (X-Y) 1 wB).
-  rewrite Zmod_small; romega.
-  contradict H1; apply Zmod_small; romega.
+  rewrite Zmod_small; lia.
+  contradict H1; apply Zmod_small; lia.
 
  generalize (Z.compare_eq ((X-Y) mod wB) (X-Y)); intros Heq.
  destruct Z.compare; intros;
@@ -1318,8 +1318,8 @@ Section Int31_Specs.
   unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros.
   destruct (Z_lt_le_dec (X-Y-1) 0).
   rewrite <- (Z_mod_plus_full (X-Y-1) 1 wB).
-  rewrite Zmod_small; romega.
-  contradict H1; apply Zmod_small; romega.
+  rewrite Zmod_small; lia.
+  contradict H1; apply Zmod_small; lia.
 
  generalize (Z.compare_eq ((X-Y-1) mod wB) (X-Y-1)); intros Heq.
  destruct Z.compare; intros;
@@ -1356,7 +1356,7 @@ Section Int31_Specs.
  change [|1|] with 1; change [|0|] with 0.
  rewrite <- (Z_mod_plus_full (0-[|x|]) 1 wB).
  rewrite Zminus_mod_idemp_l.
- rewrite Zmod_small; generalize (phi_bounded x); romega.
+ rewrite Zmod_small; generalize (phi_bounded x); lia.
  Qed.
 
  Lemma spec_pred_c : forall x, [-|sub31c x 1|] = [|x|] - 1.
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index e93ebb1ad5..0c9aca2657 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import Nnat ZArith_base ROmega ZArithRing Zdiv Morphisms.
+Require Import Nnat ZArith_base Lia ZArithRing Zdiv Morphisms.
 
 Local Open Scope Z_scope.
 
@@ -129,33 +129,33 @@ Qed.
 Theorem Zrem_lt_pos a b : 0<=a -> b<>0 -> 0 <= Z.rem a b < Z.abs b.
 Proof.
   intros; generalize (Z.rem_nonneg a b) (Z.rem_bound_abs a b);
-   romega with *.
+    lia.
 Qed.
 
 Theorem Zrem_lt_neg a b : a<=0 -> b<>0 -> -Z.abs b < Z.rem a b <= 0.
 Proof.
   intros; generalize (Z.rem_nonpos a b) (Z.rem_bound_abs a b);
-   romega with *.
+   lia.
 Qed.
 
 Theorem Zrem_lt_pos_pos a b : 0<=a -> 0<b -> 0 <= Z.rem a b < b.
 Proof.
-  intros; generalize (Zrem_lt_pos a b); romega with *.
+  intros; generalize (Zrem_lt_pos a b); lia.
 Qed.
 
 Theorem Zrem_lt_pos_neg a b : 0<=a -> b<0 -> 0 <= Z.rem a b < -b.
 Proof.
-  intros; generalize (Zrem_lt_pos a b); romega with *.
+  intros; generalize (Zrem_lt_pos a b); lia.
 Qed.
 
 Theorem Zrem_lt_neg_pos a b : a<=0 -> 0<b -> -b < Z.rem a b <= 0.
 Proof.
-  intros; generalize (Zrem_lt_neg a b); romega with *.
+  intros; generalize (Zrem_lt_neg a b); lia.
 Qed.
 
 Theorem Zrem_lt_neg_neg a b : a<=0 -> b<0 -> b < Z.rem a b <= 0.
 Proof.
-  intros; generalize (Zrem_lt_neg a b); romega with *.
+  intros; generalize (Zrem_lt_neg a b); lia.
 Qed.
 
 
@@ -171,12 +171,12 @@ Lemma Remainder_equiv : forall a b r,
  Remainder a b r <-> Remainder_alt a b r.
 Proof.
   unfold Remainder, Remainder_alt; intuition.
-  - romega with *.
-  - romega with *.
-  - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; romega.
+  - lia.
+  - lia.
+  - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; lia.
   - assert (0 <= Z.sgn r * Z.sgn a).
     { rewrite <-Z.sgn_mul, Z.sgn_nonneg; auto. }
-    destruct r; simpl Z.sgn in *; romega with *.
+    destruct r; simpl Z.sgn in *; lia.
 Qed.
 
 Theorem Zquot_mod_unique_full a b q r :
@@ -185,7 +185,7 @@ Proof.
   destruct 1 as [(H,H0)|(H,H0)]; intros.
   apply Zdiv_mod_unique with b; auto.
   apply Zrem_lt_pos; auto.
-  romega with *.
+  lia.
   rewrite <- H1; apply Z.quot_rem'.
 
   rewrite <- (Z.opp_involutive a).
@@ -193,7 +193,7 @@ Proof.
   generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Z.rem (-a) b)).
   generalize (Zrem_lt_pos (-a) b).
   rewrite <-Z.quot_rem', Z.mul_opp_r, <-Z.opp_add_distr, <-H1.
-  romega with *.
+  lia.
 Qed.
 
 Theorem Zquot_unique_full a b q r :