Numbers.Cyclic: use “lia” rather than “omega”

2 files changed, 12 insertions, 10 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index daca0ee5dc..44784675b0 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -18,6 +18,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
+Require Import Lia.
 Require Import Znumtheory.
 Require Import Zpow_facts.
 Require Import DoubleType.
@@ -298,8 +299,7 @@ Module ZnZ.
  replace (base digits) with (1 * base digits + 0) by ring.
  rewrite Hp1.
  apply Z.add_le_mono.
- apply Z.mul_le_mono_nonneg; auto with zarith.
- case p1; simpl; intros; red; simpl; intros; discriminate.
+ apply Z.mul_le_mono_nonneg. 1-2, 4: lia.
  unfold base; auto with zarith.
  case (spec_to_Z w1); auto with zarith.
  Qed.
@@ -314,7 +314,7 @@ Module ZnZ.
    forall p, 0 <= p < base digits -> [|of_Z p|] = p.
  Proof.
  intros p; case p; simpl; try rewrite spec_0; auto.
- intros; rewrite of_pos_correct; auto with zarith.
+ intros; rewrite of_pos_correct; lia.
  intros p1 (H1, _); contradict H1; apply Z.lt_nge; red; simpl; auto.
  Qed.
 
@@ -423,7 +423,7 @@ Lemma eqb_eq : forall x y, eqb x y = true <-> x == y.
 Proof.
  intros. unfold eqb, eq.
  rewrite ZnZ.spec_compare.
- case Z.compare_spec; intuition; try discriminate.
+ case Z.compare_spec; split; (easy || lia).
 Qed.
 
 Lemma eqb_correct : forall x y, eqb x y = true -> x==y.
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 53a71ce0c9..4fd2cc0564 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -15,6 +15,7 @@ Require Import ZArith.
 Require Import Zpow_facts.
 Require Import DoubleType.
 Require Import CyclicAxioms.
+Require Import Lia.
 
 (** * From [CyclicType] to [NZAxiomsSig] *)
 
@@ -59,7 +60,8 @@ Ltac zcongruence := repeat red; intros; zify; congruence.
 
 Instance eq_equiv : Equivalence eq.
 Proof.
-unfold eq. firstorder.
+  split. 1-2: firstorder.
+  intros x y z; apply eq_trans.
 Qed.
 
 Local Obligation Tactic := zcongruence.
@@ -77,7 +79,7 @@ Qed.
 
 Theorem gt_wB_0 : 0 < wB.
 Proof.
-pose proof gt_wB_1; auto with zarith.
+pose proof gt_wB_1; lia.
 Qed.
 
 Lemma one_mod_wB : 1 mod wB = 1.
@@ -138,8 +140,8 @@ intros n H1 H2 H3.
 unfold B in *. apply AS in H3.
 setoid_replace (ZnZ.of_Z (n + 1)) with (S (ZnZ.of_Z n)). assumption.
 zify.
-rewrite 2 ZnZ.of_Z_correct; auto with zarith.
-symmetry; apply Zmod_small; auto with zarith.
+rewrite 2 ZnZ.of_Z_correct. 2-3: lia.
+symmetry; apply Zmod_small; lia.
 Qed.
 
 Theorem Zbounded_induction :
@@ -155,8 +157,8 @@ apply natlike_rec2; unfold Q'.
 destruct (Z.le_gt_cases b 0) as [H | H]. now right. left; now split.
 intros n H IH. destruct IH as [[IH1 IH2] | IH].
 destruct (Z.le_gt_cases (b - 1) n) as [H1 | H1].
-right; auto with zarith.
-left. split; [auto with zarith | now apply (QS n)].
+right; lia.
+left. split; [ lia | now apply (QS n)].
 right; auto with zarith.
 unfold Q' in *; intros n H1 H2. destruct (H n H1) as [[H3 H4] | H3].
 assumption. now apply Z.le_ngt in H3.