6 files changed, 11 insertions, 10 deletions
diff --git a/plugins/micromega/DeclConstant.v b/plugins/micromega/DeclConstant.v
index 0288728504..7ad5e313e3 100644
--- a/plugins/micromega/DeclConstant.v
+++ b/plugins/micromega/DeclConstant.v
@@ -51,7 +51,7 @@ Instance GT_APP2 {T1 T2 T3: Type} (F : T1 -> T2 -> T3)
          GT A1 -> GT A2 -> GT (F A1 A2).
 Defined.
 
-Require Import ZArith.
+Require Import QArith_base.
 
 Instance DO : DeclaredConstant O := {}.
 Instance DS : DeclaredConstant S := {}.
@@ -64,6 +64,4 @@ Instance DZneg: DeclaredConstant Zneg := {}.
 Instance DZpow_pos : DeclaredConstant Z.pow_pos := {}.
 Instance DZpow     : DeclaredConstant Z.pow     := {}.
 
-Require Import QArith.
-
 Instance DQ : DeclaredConstant Qmake := {}.
diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v
index 3351c7ef8a..55a93eade7 100644
--- a/plugins/micromega/Lia.v
+++ b/plugins/micromega/Lia.v
@@ -15,7 +15,7 @@
 (************************************************************************)
 
 Require Import ZMicromega.
-Require Import ZArith.
+Require Import ZArith_base.
 Require Import RingMicromega.
 Require Import VarMap.
 Require Import DeclConstant.
diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index 3651b54ed8..6c1852acbf 100644
--- a/plugins/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.v
@@ -22,6 +22,7 @@ Require Import QArith.
 Require Import Qfield.
 Require Import Qreals.
 Require Import DeclConstant.
+Require Import Lia.
 
 Require Setoid.
 (*Declare ML Module "micromega_plugin".*)
@@ -192,7 +193,7 @@ Proof.
   destruct z ; try congruence.
   compute. congruence.
   compute. congruence.
-  generalize (Zle_0_nat n). auto with zarith.
+  generalize (Zle_0_nat n). auto using Z.le_ge.
 Qed.
 
 Definition CInvR0 (r : Rcst) := Qeq_bool (Q_of_Rcst r) (0 # 1).
@@ -333,7 +334,7 @@ Proof.
       apply Qeq_bool_eq in C2.
       rewrite C2.
       simpl.
-      rewrite Qpower0 by auto with zarith.
+      rewrite Qpower0 by lia.
       apply Q2R_0.
     + rewrite Q2RpowerRZ.
       rewrite IHc.
@@ -341,7 +342,7 @@ Proof.
       rewrite andb_false_iff in C.
       destruct C.
       simpl. apply Z.ltb_ge in H.
-      auto with zarith.
+      lia.
       left ; apply Qeq_bool_neq; auto.
     + simpl.
       rewrite <- IHc.
diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
index f93fe021f9..6db62e8401 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -15,7 +15,7 @@
 (*                                                                      *)
 (************************************************************************)
 
-Require Import ZArith.
+Require Import ZArith_base.
 Require Import Coq.Arith.Max.
 Require Import List.
 Set Implicit Arguments.
diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index 26970faf0c..08f3f39204 100644
--- a/plugins/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.v
@@ -12,9 +12,10 @@
 
 Require Import OrderedRing.
 Require Import RingMicromega.
-Require Import ZArith.
+Require Import ZArith_base.
 Require Import InitialRing.
 Require Import Setoid.
+Require Import ZArithRing.
 
 Import OrderedRingSyntax.
 
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index c160e11467..d709fdda14 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -21,7 +21,8 @@ Require Import RingMicromega.
 Require  FSetPositive FSetEqProperties.
 Require Import ZCoeff.
 Require Import Refl.
-Require Import ZArith.
+Require Import ZArith_base.
+Require Import ZArithRing.
 Require PreOmega.
 (*Declare ML Module "micromega_plugin".*)
 Local Open Scope Z_scope.