Merge PR #10983: QArith, Lia: depend on ZArith_base rather than on ZArith

Ack-by: fajb
Reviewed-by: ppedrot

14 files changed, 83 insertions, 103 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/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.
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index 72c496d56d..febf4fa1be 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -15,6 +15,7 @@ Require Export DoubleType.
 Require Import Lia.
 Require Import Zpow_facts.
 Require Import Zgcd_alt.
+Require ZArith.
 Import Znumtheory.
 
 Register bool as kernel.ind_bool.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 54d35cded2..4239943d03 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Export ZArith.
+Require Export ZArith_base.
 Require Export ZArithRing.
 Require Export Morphisms Setoid Bool.
 
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index 8d68038582..35f113e226 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 Require Import QArith.
+Import Zdiv.
 
 Lemma Qopp_lt_compat: forall p q : Q, p < q -> - q < - p.
 Proof.
@@ -38,7 +39,7 @@ Proof.
 intros z.
 unfold Qceiling.
 simpl.
-rewrite Zdiv_1_r.
+rewrite Z.div_1_r.
 apply Z.opp_involutive.
 Qed.
 
@@ -50,8 +51,7 @@ unfold Qle.
 simpl.
 replace (n*1)%Z with n by ring.
 rewrite Z.mul_comm.
-apply Z_mult_div_ge.
-auto with *.
+now apply Z.mul_div_le.
 Qed.
 
 Hint Resolve Qfloor_le : qarith.
diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v
index cc216b21f8..e889150d92 100644
--- a/theories/Structures/OrderedTypeEx.v
+++ b/theories/Structures/OrderedTypeEx.v
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 Require Import OrderedType.
-Require Import ZArith.
+Require Import ZArith_base.
 Require Import PeanoNat.
 Require Import Ascii String.
 Require Import NArith Ndec.
diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v
index 056e67db83..4896301aa7 100644
--- a/theories/ZArith/Zdigits.v
+++ b/theories/ZArith/Zdigits.v
@@ -15,11 +15,11 @@
 Require Import Bvector.
 Require Import ZArith.
 Require Export Zpower.
-Require Import Omega.
+Require Import Lia.
 
 (** The evaluation of boolean vector is done both in binary and
     two's complement. The computed number belongs to Z.
-    We hence use Omega to perform computations in Z.
+    We hence use lia to perform computations in Z.
     Moreover, we use functions [2^n] where [n] is a natural number
     (here the vector length).
 *)
@@ -155,10 +155,10 @@ Section Z_BRIC_A_BRAC.
     forall (n:nat) (bv:Bvector n), (binary_value n bv >= 0)%Z.
   Proof.
     induction bv as [| a n v IHbv]; cbn.
-    omega.
+    lia.
 
-    destruct a; destruct (binary_value n v); simpl; auto.
-    auto with zarith.
+    destruct a; destruct (binary_value n v); auto.
+    discriminate.
   Qed.
 
   Lemma two_compl_value_Sn :
@@ -203,7 +203,7 @@ Section Z_BRIC_A_BRAC.
     auto.
 
     destruct p; auto.
-    simpl; intros; omega.
+    simpl; intros; lia.
 
     intro H; elim H; trivial.
   Qed.
@@ -214,11 +214,11 @@ Section Z_BRIC_A_BRAC.
       (z < two_power_nat (S n))%Z -> (Z.div2 z < two_power_nat n)%Z.
   Proof.
     intros.
-    enough (2 * Z.div2 z < 2 * two_power_nat n)%Z by omega.
+    enough (2 * Z.div2 z < 2 * two_power_nat n)%Z by lia.
     rewrite <- two_power_nat_S.
     destruct (Zeven.Zeven_odd_dec z) as [Heven|Hodd]; intros.
     rewrite <- Zeven.Zeven_div2; auto.
-    generalize (Zeven.Zodd_div2 z Hodd); omega.
+    generalize (Zeven.Zodd_div2 z Hodd); lia.
   Qed.
 
   Lemma Z_to_two_compl_Sn_z :
@@ -253,9 +253,9 @@ Section Z_BRIC_A_BRAC.
     intros n z; rewrite (two_power_nat_S n).
     generalize (Zmod2_twice z).
     destruct (Zeven.Zeven_odd_dec z) as [H| H].
-    rewrite (Zeven_bit_value z H); intros; omega.
+    rewrite (Zeven_bit_value z H); intros; lia.
 
-    rewrite (Zodd_bit_value z H); intros; omega.
+    rewrite (Zodd_bit_value z H); intros; lia.
   Qed.
 
   Lemma Zlt_two_power_nat_S :
@@ -265,9 +265,9 @@ Section Z_BRIC_A_BRAC.
     intros n z; rewrite (two_power_nat_S n).
     generalize (Zmod2_twice z).
     destruct (Zeven.Zeven_odd_dec z) as [H| H].
-    rewrite (Zeven_bit_value z H); intros; omega.
+    rewrite (Zeven_bit_value z H); intros; lia.
 
-    rewrite (Zodd_bit_value z H); intros; omega.
+    rewrite (Zodd_bit_value z H); intros; lia.
   Qed.
 
 End Z_BRIC_A_BRAC.
@@ -309,7 +309,7 @@ Section COHERENT_VALUE.
       (z < two_power_nat n)%Z -> binary_value n (Z_to_binary n z) = z.
   Proof.
     induction n as [| n IHn].
-    unfold two_power_nat, shift_nat; simpl; intros; omega.
+    unfold two_power_nat, shift_nat; simpl; intros; lia.
 
     intros; rewrite Z_to_binary_Sn_z.
     rewrite binary_value_Sn.
@@ -328,13 +328,13 @@ Section COHERENT_VALUE.
   Proof.
     induction n as [| n IHn].
     unfold two_power_nat, shift_nat; simpl; intros.
-    assert (z = (-1)%Z \/ z = 0%Z). omega.
+    assert (z = (-1)%Z \/ z = 0%Z). lia.
     intuition; subst z; trivial.
 
     intros; rewrite Z_to_two_compl_Sn_z.
     rewrite two_compl_value_Sn.
     rewrite IHn.
-    generalize (Zmod2_twice z); omega.
+    generalize (Zmod2_twice z); lia.
 
     apply Zge_minus_two_power_nat_S; auto.
 
diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v
index 0cc137ef5d..da2df40572 100644
--- a/theories/ZArith/Zgcd_alt.v
+++ b/theories/ZArith/Zgcd_alt.v
@@ -25,7 +25,7 @@ Require Import ZArith_base.
 Require Import ZArithRing.
 Require Import Zdiv.
 Require Import Znumtheory.
-Require Import Omega.
+Require Import Lia.
 
 Open Scope Z_scope.
 
@@ -76,8 +76,7 @@ Open Scope Z_scope.
    Z.abs a < Z.of_nat n -> Zis_gcd a b (Zgcdn n a b).
  Proof.
    induction n.
-   simpl; intros.
-   exfalso; generalize (Z.abs_nonneg a); omega.
+   intros; lia.
    destruct a; intros; simpl;
      [ generalize (Zis_gcd_0_abs b); intuition | | ];
    unfold Z.modulo;
@@ -85,8 +84,7 @@ Open Scope Z_scope.
    destruct (Z.div_eucl b (Zpos p)) as (q,r);
    intros (H0,H1);
    rewrite Nat2Z.inj_succ in H; simpl Z.abs in H;
-   (assert (H2: Z.abs r < Z.of_nat n) by
-    (rewrite Z.abs_eq; auto with zarith));
+   (assert (H2: Z.abs r < Z.of_nat n) by lia);
     assert (IH:=IHn r (Zpos p) H2); clear IHn;
     simpl in IH |- *;
     rewrite H0.
@@ -108,15 +106,11 @@ Open Scope Z_scope.
  Lemma fibonacci_pos : forall n, 0 <= fibonacci n.
  Proof.
    enough (forall N n, (n<N)%nat -> 0<=fibonacci n) by eauto.
-   induction N.
-   inversion 1.
+   induction N. intros; lia.
+   intros [ | [ | n ] ]. 1-2: simpl; lia.
    intros.
-   destruct n.
-   simpl; auto with zarith.
-   destruct n.
-   simpl; auto with zarith.
    change (0 <= fibonacci (S n) + fibonacci n).
-   generalize (IHN n) (IHN (S n)); omega.
+   generalize (IHN n) (IHN (S n)); lia.
  Qed.
 
  Lemma fibonacci_incr :
@@ -129,7 +123,7 @@ Open Scope Z_scope.
    destruct m.
    simpl; auto with zarith.
    change (fibonacci (S m) <= fibonacci (S m)+fibonacci m).
-   generalize (fibonacci_pos m); omega.
+   generalize (fibonacci_pos m); lia.
  Qed.
 
  (** 3) We prove that fibonacci numbers are indeed worst-case:
@@ -144,8 +138,8 @@ Open Scope Z_scope.
    fibonacci (S (S n)) <= b.
  Proof.
    induction n.
-   intros [|a|a]; intros; simpl; omega.
-   intros [|a|a] b (Ha,Ha'); [simpl; omega | | easy ].
+   intros [|a|a]; intros; simpl; lia.
+   intros [|a|a] b (Ha,Ha'); [simpl; lia | | easy ].
    remember (S n) as m.
    rewrite Heqm at 2. simpl Zgcdn.
    unfold Z.modulo; generalize (Z_div_mod b (Zpos a) eq_refl).
@@ -161,20 +155,13 @@ Open Scope Z_scope.
        apply Zis_gcd_sym.
        apply Zis_gcd_for_euclid2; auto.
        apply Zis_gcd_sym; auto.
-     + split; auto.
-       rewrite EQ.
-       apply Z.add_le_mono; auto.
-       apply Z.le_trans with (Zpos a * 1); auto.
-       now rewrite Z.mul_1_r.
-       apply Z.mul_le_mono_nonneg_l; auto with zarith.
-       change 1 with (Z.succ 0). apply Z.le_succ_l.
-       destruct q; auto with zarith.
-       assert (Zpos a * Zneg p < 0) by now compute. omega.
+     + split. auto.
+       destruct q. lia. 1-2: nia.
    - (* r = 0 *)
      clear IHn EQ Hr'; intros _.
      subst r; simpl; rewrite Heqm.
      destruct n.
-     + simpl. omega.
+     + simpl. lia.
      + now destruct 1.
  Qed.
 
@@ -184,7 +171,7 @@ Open Scope Z_scope.
    0 < a < b -> a < fibonacci (S n) ->
    Zis_gcd a b (Zgcdn n a b).
  Proof.
-   destruct a; [ destruct 1; exfalso; omega | | destruct 1; discriminate].
+   destruct a. 1,3 : intros; lia.
    cut (forall k n b,
      k = (S (Pos.to_nat p) - n)%nat ->
      0 < Zpos p < b -> Zpos p < fibonacci (S n) ->
@@ -192,22 +179,17 @@ Open Scope Z_scope.
    destruct 2; eauto.
    clear n; induction k.
    intros.
-   assert (Pos.to_nat p < n)%nat by omega.
    apply Zgcdn_linear_bound.
-   simpl.
-   generalize (inj_le _ _ H2).
-   rewrite Nat2Z.inj_succ.
-   rewrite positive_nat_Z; auto.
-   omega.
+   lia.
    intros.
    generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros.
    assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)).
    apply IHk; auto.
-   omega.
+   lia.
    replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto.
-   generalize (fibonacci_pos n); omega.
+   generalize (fibonacci_pos n); lia.
    replace (Zgcdn n (Zpos p) b) with (Zgcdn (S n) (Zpos p) b); auto.
-   generalize (H2 H3); clear H2 H3; omega.
+   generalize (H2 H3); clear H2 H3; lia.
  Qed.
 
  (** 4) The proposed bound leads to a fibonacci number that is big enough. *)
@@ -215,7 +197,7 @@ Open Scope Z_scope.
  Lemma Zgcd_bound_fibonacci :
    forall a, 0 < a -> a < fibonacci (Zgcd_bound a).
  Proof.
-   destruct a; [omega| | intro H; discriminate].
+   destruct a; [lia| | intro H; discriminate].
    intros _.
    induction p; [ | | compute; auto ];
     simpl Zgcd_bound in *;
@@ -224,10 +206,10 @@ Open Scope Z_scope.
     assert (n <> O) by (unfold n; destruct p; simpl; auto).
 
    destruct n as [ |m]; [elim H; auto| ].
-   generalize (fibonacci_pos m); rewrite Pos2Z.inj_xI; omega.
+   generalize (fibonacci_pos m); rewrite Pos2Z.inj_xI; lia.
 
    destruct n as [ |m]; [elim H; auto| ].
-   generalize (fibonacci_pos m); rewrite Pos2Z.inj_xO; omega.
+   generalize (fibonacci_pos m); rewrite Pos2Z.inj_xO; lia.
  Qed.
 
  (* 5) the end: we glue everything together and take care of
@@ -265,10 +247,10 @@ Open Scope Z_scope.
   Z.le_elim H1.
   + apply Zgcdn_ok_before_fibonacci; auto.
     apply Z.lt_le_trans with (fibonacci (S m));
-    [ omega | apply fibonacci_incr; auto].
+    [ lia | apply fibonacci_incr; auto].
   + subst r; simpl.
-    destruct m as [ |m]; [exfalso; omega| ].
-    destruct n as [ |n]; [exfalso; omega| ].
+    destruct m as [ |m]; [ lia | ].
+    destruct n as [ |n]; [ lia | ].
     simpl; apply Zis_gcd_sym; apply Zis_gcd_0.
  Qed.
 
@@ -277,7 +259,7 @@ Open Scope Z_scope.
  Proof.
    destruct a.
    - simpl; intros.
-     destruct n; [exfalso; omega | ].
+     destruct n; [ lia | ].
      simpl; generalize (Zis_gcd_0_abs b); intuition.
    - apply Zgcdn_is_gcd_pos.
    - rewrite <- Zgcd_bound_opp, <- Zgcdn_opp.
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index e65eb7cdc7..a669429ffa 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import ZArith_base ZArithRing Omega Zcomplements Zdiv Znumtheory.
+Require Import ZArith_base ZArithRing Lia Zcomplements Zdiv Znumtheory.
 Require Export Zpower.
 Local Open Scope Z_scope.
 
@@ -49,7 +49,7 @@ Proof. intros. now apply Z.pow_le_mono_r. Qed.
 
 Theorem Zpower_lt_monotone a b c :
  1 < a -> 0 <= b < c -> a^b < a^c.
-Proof. intros. apply Z.pow_lt_mono_r; auto with zarith. Qed.
+Proof. intros. apply Z.pow_lt_mono_r; lia. Qed.
 
 Theorem Zpower_gt_1 x y : 1 < x -> 0 < y -> 1 < x^y.
 Proof. apply Z.pow_gt_1. Qed.
@@ -87,10 +87,10 @@ Proof.
   assert (Hn := Nat2Z.is_nonneg n).
   destruct p; simpl Pos.size_nat.
   - specialize IHn with p.
-    rewrite Pos2Z.inj_xI, Nat2Z.inj_succ, Z.pow_succ_r; omega.
+    rewrite Nat2Z.inj_succ, Z.pow_succ_r; lia.
   - specialize IHn with p.
-    rewrite Pos2Z.inj_xO, Nat2Z.inj_succ, Z.pow_succ_r; omega.
-  - split; auto with zarith.
+    rewrite Nat2Z.inj_succ, Z.pow_succ_r; lia.
+  - split. lia.
     intros _. apply Z.pow_gt_1. easy.
     now rewrite Nat2Z.inj_succ, Z.lt_succ_r.
 Qed.
@@ -103,8 +103,8 @@ Proof.
   intros Hn; destruct (Z.le_gt_cases 0 q) as [H1|H1].
   - pattern q; apply natlike_ind; trivial.
     clear q H1. intros q Hq Rec. rewrite !Z.pow_succ_r; trivial.
-    rewrite Z.mul_mod_idemp_l; auto with zarith.
-    rewrite Z.mul_mod, Rec, <- Z.mul_mod; auto with zarith.
+    rewrite Z.mul_mod_idemp_l by lia.
+    rewrite Z.mul_mod, Rec, <- Z.mul_mod by lia. reflexivity.
   - rewrite !Z.pow_neg_r; auto with zarith.
 Qed.
 
@@ -163,7 +163,7 @@ Qed.
 Lemma Zpower_divide p q : 0 < q -> (p | p ^ q).
 Proof.
   exists (p^(q - 1)).
-  rewrite Z.mul_comm, <- Z.pow_succ_r; f_equal; auto with zarith.
+  rewrite Z.mul_comm, <- Z.pow_succ_r by lia; f_equal; lia.
 Qed.
 
 Theorem rel_prime_Zpower_r i p q :
@@ -190,7 +190,7 @@ Proof.
   - simpl; intros.
     assert (2<=p) by (apply prime_ge_2; auto).
     assert (p<=1) by (apply Z.divide_pos_le; auto with zarith).
-    omega.
+    lia.
   - intros n Hn Rec.
     rewrite Z.pow_succ_r by trivial. intros.
     assert (2<=p) by (apply prime_ge_2; auto).
@@ -213,11 +213,11 @@ Proof.
   exists 1; rewrite Z.pow_1_r; apply prime_power_prime with n; auto.
   case not_prime_divide with (2 := Hpr); auto.
   intros p1 ((Hp1, Hpq1),(q1,->)).
-  assert (Hq1 : 0 < q1) by (apply Z.mul_lt_mono_pos_r with p1; auto with zarith).
-  destruct (IH p1) with p n as (r1,Hr1); auto with zarith.
+  assert (Hq1 : 0 < q1) by (apply Z.mul_lt_mono_pos_r with p1; lia).
+  destruct (IH p1) with p n as (r1,Hr1). 3-4: assumption. 1-2: lia.
   transitivity (q1 * p1); trivial. exists q1; auto with zarith.
-  destruct (IH q1) with p n as (r2,Hr2); auto with zarith.
-  split; auto with zarith.
+  destruct (IH q1) with p n as (r2,Hr2). 3-4: assumption. 2: lia.
+  split. lia.
   rewrite <- (Z.mul_1_r q1) at 1.
   apply Z.mul_lt_mono_pos_l; auto with zarith.
   transitivity (q1 * p1); trivial. exists p1; auto with zarith.
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index fea7db7921..b3e7fff7d6 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -63,6 +63,7 @@ Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Z.quot_1_r Z.rem_1_r
 Ltac zero_or_not a :=
   destruct (Z.eq_decidable a 0) as [->|?];
   [rewrite ?Zquot_0_l, ?Zrem_0_l, ?Zquot_0_r, ?Zrem_0_r;
+   try lia;
    auto with zarith|].
 
 Lemma Z_rem_same a : Z.rem a a = 0.
@@ -100,7 +101,6 @@ Proof. zero_or_not b. now apply Z.rem_opp_opp. Qed.
 Theorem Zrem_sgn a b : 0 <= Z.sgn (Z.rem a b) * Z.sgn a.
 Proof.
   zero_or_not b.
-  - apply Z.square_nonneg.
   - zero_or_not (Z.rem a b).
     rewrite Z.rem_sign_nz; trivial. apply Z.square_nonneg.
 Qed.
@@ -203,18 +203,18 @@ Qed.
 (* Division of positive numbers is positive. *)
 
 Lemma Z_quot_pos a b : 0 <= a -> 0 <= b -> 0 <= a÷b.
-Proof. intros. zero_or_not b. apply Z.quot_pos; auto with zarith. Qed.
+Proof. intros. zero_or_not b. apply Z.quot_pos; lia. Qed.
 
 (** As soon as the divisor is greater or equal than 2,
     the division is strictly decreasing. *)
 
 Lemma Z_quot_lt a b : 0 < a -> 2 <= b -> a÷b < a.
-Proof. intros. apply Z.quot_lt; auto with zarith. Qed.
+Proof. intros. apply Z.quot_lt; lia. Qed.
 
 (** [<=] is compatible with a positive division. *)
 
 Lemma Z_quot_monotone a b c : 0<=c -> a<=b -> a÷c <= b÷c.
-Proof. intros. zero_or_not c. apply Z.quot_le_mono; auto with zarith. Qed.
+Proof. intros. zero_or_not c. apply Z.quot_le_mono; lia. Qed.
 
 (** With our choice of division, rounding of (a÷b) is always done toward 0: *)
 
@@ -228,12 +228,12 @@ Proof. intros. zero_or_not b. apply Z.mul_quot_ge; auto with zarith. Qed.
     iff the modulo is zero. *)
 
 Lemma Z_quot_exact_full a b : a = b*(a÷b) <-> Z.rem a b = 0.
-Proof. intros. zero_or_not b. intuition. apply Z.quot_exact; auto. Qed.
+Proof. intros. zero_or_not b. apply Z.quot_exact; auto. Qed.
 
 (** A modulo cannot grow beyond its starting point. *)
 
 Theorem Zrem_le a b : 0 <= a -> 0 <= b -> Z.rem a b <= a.
-Proof. intros. zero_or_not b. apply Z.rem_le; auto with zarith. Qed.
+Proof. intros. zero_or_not b. apply Z.rem_le; lia. Qed.
 
 (** Some additional inequalities about Zdiv. *)
 
@@ -357,7 +357,7 @@ Qed.
 
 Theorem Zquot_mult_le:
  forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a÷b) <= (c*a)÷b.
-Proof. intros. zero_or_not b. apply Z.quot_mul_le; auto with zarith. Qed.
+Proof. intros. zero_or_not b. apply Z.quot_mul_le; lia. Qed.
 
 (** Z.rem is related to divisibility (see more in Znumtheory) *)
 
@@ -376,7 +376,7 @@ Lemma Zquot2_odd_remainder : forall a,
 Proof.
  intros [ |p|p]. simpl.
  left. simpl. auto with zarith.
- left. destruct p; simpl; auto with zarith.
+ left. destruct p; simpl; lia.
  right. destruct p; simpl; split; now auto with zarith.
 Qed.
 
@@ -414,10 +414,10 @@ Theorem Zquotrem_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b ->
 Proof.
   intros.
   apply Zdiv_mod_unique with b.
-  apply Zrem_lt_pos; auto with zarith.
-  rewrite Z.abs_eq; auto with *; apply Z_mod_lt; auto with *.
-  rewrite <- Z_div_mod_eq; auto with *.
-  symmetry; apply Z.quot_rem; auto with *.
+  apply Zrem_lt_pos; lia.
+  rewrite Z.abs_eq by lia. apply Z_mod_lt; lia.
+  rewrite <- Z_div_mod_eq by lia.
+  symmetry; apply Z.quot_rem; lia.
 Qed.
 
 Theorem Zquot_Zdiv_pos : forall a b, 0 <= a -> 0 <= b ->
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
index 853ec951ae..ca04bb4c8f 100644
--- a/theories/ZArith/Zwf.v
+++ b/theories/ZArith/Zwf.v
@@ -10,7 +10,7 @@
 
 Require Import ZArith_base.
 Require Export Wf_nat.
-Require Import Omega.
+Require Import Lia.
 Local Open Scope Z_scope.
 
 (** Well-founded relations on Z. *)
@@ -39,20 +39,19 @@ Section wf_proof.
     clear a; simple induction n; intros.
   (** n= 0 *)
     case H; intros.
-    case (lt_n_O (f a)); auto.
+    lia.
     apply Acc_intro; unfold Zwf; intros.
-    assert False; omega || contradiction.
+    lia.
   (** inductive case *)
     case H0; clear H0; intro; auto.
     apply Acc_intro; intros.
     apply H.
     unfold Zwf in H1.
-    case (Z.le_gt_cases c y); intro; auto with zarith.
+    case (Z.le_gt_cases c y); intro. 2: lia.
     left.
-    red in H0.
     apply lt_le_trans with (f a); auto with arith.
     unfold f.
-    apply Zabs2Nat.inj_lt; omega.
+    lia.
     apply (H (S (f a))); auto.
   Qed.
 
@@ -83,9 +82,7 @@ Section wf_proof_up.
   Proof.
     apply well_founded_lt_compat with (f := f).
     unfold Zwf_up, f.
-    intros.
-    apply Zabs2Nat.inj_lt; try (apply Z.le_0_sub; intuition).
-    now apply Z.sub_lt_mono_l.
+    lia.
   Qed.
 
 End wf_proof_up.