Tune imports.

FEM/Algebra/nat_compl.v

@@ -21,9 +21,9 @@ Set Warnings "-notation-overridden".
 From mathcomp Require Import ssrnat.
 Set Warnings "notation-overridden".
 
-From Lebesgue Require Import nat_compl Subset_dec logic_compl.
+From Lebesgue Require Import Subset_dec logic_compl.
 
-From FEM Require Import logic_compl.
+From FEM Require Import Compl.
 
 
 (* TODO FC (05/02/2024): maybe drop the nat_ prefix, or put it everywhere... *)
@@ -169,7 +169,7 @@ Lemma nat_lt_total_strict :
 Proof. move=>>; apply Nat.lt_gt_cases. Qed.
 
 Lemma nat_eq_le : forall m n, m = n -> (m <= n)%coq_nat.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma le_neq_lt : forall m n, (m <= n)%coq_nat -> m <> n -> (m < n)%coq_nat.
 Proof. intros; apply Nat.le_neq; easy. Qed.
@@ -181,41 +181,41 @@ Lemma nat_ltS : forall n, (n < n.+1)%coq_nat.
 Proof. exact Nat.lt_succ_diag_r. Qed.
 
 Lemma nat_le_ltS : forall {n i}, (i <= n)%coq_nat -> (i < n.+1)%coq_nat.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma pred_succ : forall m n, m <> 0 -> m.-1 = n -> m = n.+1.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma succ_pred : forall m n, m = n.+1 -> m.-1 = n.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma nat_plus_reg_l :
   forall n n1 n2, (n + n1)%coq_nat = (n + n2)%coq_nat -> n1 = n2.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma nat_plus_reg_r :
   forall n n1 n2, (n1 + n)%coq_nat = (n2 + n)%coq_nat -> n1 = n2.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma nat_plus_zero_reg_l : forall m n, (m + n)%coq_nat = m -> n = 0.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma nat_plus_zero_reg_r : forall m n, (m + n)%coq_nat = n -> m = 0.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma nat_add_2_l : forall n, (2 + n)%coq_nat = n.+2.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma nat_add_2_r : forall n, (n + 2)%coq_nat = n.+2.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma nat_add_sub_equiv_l :
   forall {m n p}, (p <= m)%coq_nat -> m = (n + p)%coq_nat <-> n = (m - p)%coq_nat.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma nat_add_sub_equiv_r :
   forall {m n p}, (n <= m)%coq_nat -> m = (n + p)%coq_nat <-> p = (m - n)%coq_nat.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma nat_double_S : forall n, (2 * n.+1)%coq_nat = (2 * n)%coq_nat.+2.
 Proof. intros; rewrite Nat.mul_succ_r; apply nat_add_2_r. Qed.
@@ -226,37 +226,37 @@ Proof. intros; rewrite nat_double_S Nat.add_1_r; easy. Qed.
 
 Lemma nat_lt_lt_S :
   forall m n p, (m < n)%coq_nat -> (n < p.+1)%coq_nat -> (m < p)%coq_nat.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma nat_lt2_add_lt1_sub_l :
   forall m n p, (n <= m)%coq_nat ->
     (m < (n + p)%coq_nat)%coq_nat <-> ((m - n)%coq_nat < p)%coq_nat.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma nat_lt2_add_lt1_sub_r :
   forall m n p, (p <= m)%coq_nat ->
     (m < (n + p)%coq_nat)%coq_nat <-> ((m - p)%coq_nat < n)%coq_nat.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma nat_lt2_sub_lt1_add_l :
   forall m n p, (m < (n - p)%coq_nat)%coq_nat <-> ((m + p)%coq_nat < n)%coq_nat.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma nat_lt2_sub_lt1_add_r :
   forall m n p, (p < (n - m)%coq_nat)%coq_nat <-> ((m + p)%coq_nat < n)%coq_nat.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma sub_le_mono_r :
   forall m n p,
     (p <= m)%coq_nat -> (p <= n)%coq_nat ->
     ((m - p)%coq_nat <= (n - p)%coq_nat)%coq_nat -> (m <= n)%coq_nat.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 Lemma sub_lt_mono_r :
   forall m n p,
     (p <= m)%coq_nat -> (p <= n)%coq_nat ->
     ((m - p)%coq_nat < (n - p)%coq_nat)%coq_nat -> (m < n)%coq_nat.
-Proof. Lia.lia. Qed.
+Proof. lia. Qed.
 
 (* FC: uniqueness also holds... *)
 Lemma nat_has_greatest_element :
@@ -283,7 +283,7 @@ assert (Hm1' : Q m).
   destruct (le_lt_eq_dec m n) as [Hn' | Hn']; try easy.
   apply Hm1; easy.
   rewrite Hn' in H; easy.
-specialize (Hm2 m Hm1'); contradict Hm2; Lia.lia.
+specialize (Hm2 m Hm1'); contradict Hm2; lia.
 (* . *)
 intros n Hn; destruct (le_lt_dec n m) as [Hn' | Hn']; try easy.
 contradict Hn; apply (Hm1 n); easy.
@@ -401,10 +401,10 @@ Lemma addnS_sym : forall m n, (m + n).+1 = m + n.+1.
 Proof. intros; apply eq_sym, addnS. Qed.
 
 Lemma addn_inj_l : forall p {m n}, m + p = n + p -> m = n.
-Proof. move=>>; rewrite -plusE; Lia.lia. Qed.
+Proof. move=>>; rewrite -plusE; lia. Qed.
 
 Lemma addn_inj_r : forall p {m n}, p + m = p + n -> m = n.
-Proof. move=>>; rewrite -plusE; Lia.lia. Qed.
+Proof. move=>>; rewrite -plusE; lia. Qed.
 
 Lemma addn1K : forall n, (n + 1).-1 = n.
 Proof. intros; rewrite addn1 //. Qed.