From 1a65950147c0b1ce9ebd356fc21d2a762cbb14c7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Wed, 14 Feb 2024 19:46:23 +0100
Subject: [PATCH] Use sym_eq when eqtype is required, otherwise use eq_sym.

---
 FEM/Algebra/AffineSpace.v       | 24 ++++++------
 FEM/Algebra/Finite_dim.v        | 40 +++++++++----------
 FEM/Algebra/Finite_family.v     | 68 ++++++++++++++++-----------------
 FEM/Algebra/ModuleSpace_compl.v | 20 +++++-----
 FEM/Algebra/Monoid_compl.v      | 16 ++++----
 FEM/Algebra/Ring_compl.v        |  2 +-
 FEM/Algebra/nat_compl.v         |  4 +-
 FEM/Compl/Function_compl.v      |  2 +-
 FEM/Compl/Function_sub.v        |  2 +-
 9 files changed, 89 insertions(+), 89 deletions(-)

diff --git a/FEM/Algebra/AffineSpace.v b/FEM/Algebra/AffineSpace.v
index 7fe68c58..35186d89 100644
--- a/FEM/Algebra/AffineSpace.v
+++ b/FEM/Algebra/AffineSpace.v
@@ -133,7 +133,7 @@ Lemma vect_zero_equiv : forall (A B : E), A --> B = 0 <-> B = A.
 Proof.
 intros A B; split; intros H.
 (* *)
-apply sym_eq; destruct (vect_l_bij_ex A 0) as [C [_ HC]].
+apply eq_sym; destruct (vect_l_bij_ex A 0) as [C [_ HC]].
 rewrite -(HC A (vect_zero _)); apply HC; easy.
 (* *)
 rewrite H; apply vect_zero.
@@ -640,7 +640,7 @@ Lemma vectF_change_orig :
   forall {n} O1 O2 (A : 'E^n), vectF O2 A = constF n (O2 --> O1) + vectF O1 A.
 Proof.
 intros; apply extF; intro; rewrite fct_plus_eq !vectF_correct constF_correct.
-apply sym_eq, vect_chasles.
+apply eq_sym, vect_chasles.
 Qed.
 
 Lemma vectF_chasles :
@@ -897,7 +897,7 @@ Lemma translF_w_zero_struct_r :
   forall {n} (O O' : E) (u : 'V^n), zero_struct K -> translF O u = constF n O'.
 Proof.
 intros n O O' u HK; move: (@ms_w_zero_struct_r _ V HK) => HV.
-apply sym_eq, translF_vectF_equiv, extF; intros i.
+apply eq_sym, translF_vectF_equiv, extF; intros i.
 rewrite vectF_w_zero_struct_r; easy.
 Qed.
 
@@ -988,7 +988,7 @@ Qed.
 Lemma frameF_inv_frameF :
   forall {n} (O : E) (u : 'V^n) i0, frameF (inv_frameF O u i0) i0 = u.
 Proof.
-intros; unfold frameF, inv_frameF; apply sym_eq, translF_vectF_equiv.
+intros; unfold frameF, inv_frameF; apply eq_sym, translF_vectF_equiv.
 rewrite translF_correct (insertF_correct_l _ _ (erefl _)).
 rewrite -{1}(transl_zero O) translF_insertF skipF_insertF; easy.
 Qed.
@@ -996,7 +996,7 @@ Qed.
 Lemma inv_frameF_frameF :
   forall {n} (A : 'E^n.+1) i0, inv_frameF (A i0) (frameF A i0) i0 = A.
 Proof.
-intros; unfold frameF, inv_frameF; apply sym_eq, translF_vectF_equiv.
+intros; unfold frameF, inv_frameF; apply eq_sym, translF_vectF_equiv.
 rewrite -(vect_zero (A i0)) -vectF_insertF insertF_skipF; easy.
 Qed.
 
@@ -1129,7 +1129,7 @@ Lemma is_comb_aff_uniq :
     invertible (sum L) -> is_comb_aff L A G1 -> is_comb_aff L A G2 -> G1 = G2.
 Proof.
 unfold is_comb_aff; intros n L A G1 G2 HL HG1 HG2.
-apply sym_eq, vect_zero_equiv, (scal_zero_reg_r (sum L)); try easy.
+apply eq_sym, vect_zero_equiv, (scal_zero_reg_r (sum L)); try easy.
 rewrite scal_sum_l -(minus_eq_zero 0) -{1}HG1 -HG2 -comb_lin_minus_r; f_equal.
 rewrite -plus_minus_r_equiv plus_comm; apply vectF_change_orig.
 Qed.
@@ -1360,7 +1360,7 @@ Lemma barycenter_kron_l :
   forall {n} (A : 'E^n) (j : 'I_n), barycenter ((kron K)^~ j) A = A j.
 Proof.
 intros n A j; destruct n as [|n]; try now destruct j.
-apply sym_eq, (barycenter_correct_orig_equiv (A ord0)); rewrite sum_kron_l.
+apply eq_sym, (barycenter_correct_orig_equiv (A ord0)); rewrite sum_kron_l.
 apply invertible_one.
 rewrite scal_one comb_lin_kron_in_l; easy.
 Qed.
@@ -1369,7 +1369,7 @@ Lemma barycenter_kron_r :
   forall {n} (A : 'E^n) (i : 'I_n), barycenter (kron K i) A = A i.
 Proof.
 intros n A i; destruct n as [|n]; try now destruct i.
-apply sym_eq, (barycenter_correct_orig_equiv (A ord0)); rewrite sum_kron_r.
+apply eq_sym, (barycenter_correct_orig_equiv (A ord0)); rewrite sum_kron_r.
 apply invertible_one.
 rewrite scal_one comb_lin_kron_in_r; easy.
 Qed.
@@ -1577,7 +1577,7 @@ Lemma barycenter_singleF :
     invertible a -> L = singleF a -> B = singleF A -> barycenter L B = A.
 Proof.
 intros; apply barycenter_constF; subst; try now apply sum_singleF_invertible.
-apply sym_eq, constF_1.
+apply eq_sym, constF_1.
 Qed.
 
 Lemma barycenter_permutF :
@@ -1585,7 +1585,7 @@ Lemma barycenter_permutF :
     injective p -> invertible (sum L) ->
     barycenter (permutF p L) (permutF p A) = barycenter L A.
 Proof.
-intros n p L A Hp HL; apply sym_eq, barycenter_correct_equiv.
+intros n p L A Hp HL; apply eq_sym, barycenter_correct_equiv.
 rewrite sum_permutF; easy.
 apply is_comb_aff_permutF; try easy.
 apply barycenter_correct; easy.
@@ -1629,7 +1629,7 @@ pose (Hq1b := bij_inj Hq1a).
 rewrite 2!comb_lin_castF_l.
 rewrite -(comb_lin_permutF Hq1b) -comb_lin_filter_n0F_l in HG1.
 rewrite -HG1; f_equal; rewrite -castF_sym_equiv.
-apply sym_eq; rewrite -castF_sym_equiv.
+apply eq_sym; rewrite -castF_sym_equiv.
 rewrite filter_n0F_gen_unfun0F_l; repeat f_equal.
 apply extF; intros i1; rewrite !vectF_correct Hf; easy.
 Qed.
@@ -2143,7 +2143,7 @@ Qed.
 Lemma barycenter_ms_eq :
   forall {n} L (A : 'E^n), sum L = 1 -> barycenter L A = comb_lin L A.
 Proof.
-intros n L A HL; apply sym_eq, barycenter_correct_equiv.
+intros n L A HL; apply eq_sym, barycenter_correct_equiv.
 rewrite HL; apply invertible_one.
 unfold is_comb_aff; rewrite vectF_ms_eq comb_lin_minus_r.
 rewrite minus_zero_equiv -scal_sum_l HL scal_one; easy.
diff --git a/FEM/Algebra/Finite_dim.v b/FEM/Algebra/Finite_dim.v
index b8718b69..f11683fd 100644
--- a/FEM/Algebra/Finite_dim.v
+++ b/FEM/Algebra/Finite_dim.v
@@ -285,7 +285,7 @@ Lemma span_castF_compat :
 Proof.
 intros n1 n2 Hn B1; apply subset_ext_equiv; split; intros _ [L]; apply span_ex.
 subst n1; exists L; apply comb_lin_eq_r, castF_refl.
-subst n2; exists L; apply comb_lin_eq_r, sym_eq, castF_refl.
+subst n2; exists L; apply comb_lin_eq_r, eq_sym, castF_refl.
 Qed.
 
 Lemma span_concatF_sym :
@@ -529,14 +529,14 @@ Lemma is_generator_concatF_compat_l :
   forall {B1 : 'E^n1} {B2 : 'E^n2},
     inclF B2 PE -> is_generator PE B1 -> is_generator PE (concatF B1 B2).
 Proof.
-move=>> HB2 HB1; rewrite HB1; apply sym_eq, span_concatF_l; rewrite -HB1; easy.
+move=>> HB2 HB1; rewrite HB1; apply eq_sym, span_concatF_l; rewrite -HB1; easy.
 Qed.
 
 Lemma is_generator_concatF_compat_r :
   forall {B1 : 'E^n1} {B2 : 'E^n2},
     inclF B1 PE -> is_generator PE B2 -> is_generator PE (concatF B1 B2).
 Proof.
-move=>> HB1 HB2; rewrite HB2; apply sym_eq, span_concatF_r; rewrite -HB2; easy.
+move=>> HB1 HB2; rewrite HB2; apply eq_sym, span_concatF_r; rewrite -HB2; easy.
 Qed.
 
 Lemma is_generator_zero_closed : forall (B : 'E^n), is_generator PE B -> PE 0.
@@ -769,7 +769,7 @@ Lemma is_lin_dep_castF_reg :
   forall {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
     is_lin_dep (castF H B1) -> is_lin_dep B1.
 Proof.
-intros n1 n2 H B1 HB; rewrite -(castF_id _ (sym_eq H) B1).
+intros n1 n2 H B1 HB; rewrite -(castF_id _ (eq_sym H) B1).
 apply is_lin_dep_castF_compat; easy.
 Qed.
 
@@ -1818,7 +1818,7 @@ Lemma is_lin_dep_gt_span :
   forall {n1 n2} (B1 : 'E^n1) {B2 : 'E^n2},
     (n1 < n2)%coq_nat -> inclF B2 (span B1) -> is_lin_dep B2.
 Proof.
-move=>> /ltP Hn HB; apply is_lin_dep_castF_reg with (sym_eq (subnKC Hn)).
+move=>> /ltP Hn HB; apply is_lin_dep_castF_reg with (eq_sym (subnKC Hn)).
 eapply is_lin_dep_ext; try (symmetry; apply concatF_splitF).
 eapply is_lin_dep_concatF_compat_l, is_lin_dep_S_span; intros i2.
 unfold firstF, castF; apply HB.
@@ -2137,7 +2137,7 @@ Lemma is_free_is_basis :
 Proof.
 move=>> HPE Hf1 Hf2; generalize HPE; intros [B [HB _]].
 destruct (incomplete_basis_theorem HPE Hf1 Hf2 HB) as [m [C [Hm [_ [_ HC]]]]].
-apply sym_eq, nat_plus_zero_reg_l in Hm; subst m.
+apply eq_sym, nat_plus_zero_reg_l in Hm; subst m.
 rewrite concatF_nil_r is_basis_castF_equiv in HC; easy.
 Qed.
 
@@ -2160,7 +2160,7 @@ Lemma is_free_overbasis_ex_alt :
 Proof.
 intros n nf Bf HPE Hf1 Hf2.
 destruct (is_free_overbasis_ex HPE Hf1 Hf2) as [m [C [Hm [_ HC]]]].
-exists (castF (sym_eq Hm) (concatF Bf C)); split.
+exists (castF (eq_sym Hm) (concatF Bf C)); split.
 apply invalF_castF_r_equiv, concatF_ub_l.
 apply is_basis_castF_compat; easy.
 Qed.
@@ -2228,7 +2228,7 @@ assert (Hf1 : inclF (singleF (Bg i)) PE).
 assert (Hf2 : is_free (singleF (Bg i))) by now apply is_free_singleF_equiv.
 destruct (incomplete_basis_theorem HPE Hf1 Hf2 Hg)
     as [m [C [Hm [_ [HC1 HC2]]]]].
-exists (castF (sym_eq Hm) (concatF (singleF (Bg i)) C)); split.
+exists (castF (eq_sym Hm) (concatF (singleF (Bg i)) C)); split.
 apply invalF_castF_l_equiv, concatF_lub_invalF; try easy.
 apply invalF_singleF_refl.
 apply is_basis_castF_equiv; easy.
@@ -2715,7 +2715,7 @@ move: (has_dim_compatible_ms HPE) => HPE'.
 intros nr nk Hnr Hnk.
 assert (Hn : (nk <= nPE)%coq_nat)
     by apply (has_dim_monot _ (KerS_incl _ _) Hnk HPE).
-apply sym_eq, (nat_add_sub_equiv_l Hn), (dim_is_unique Hnr).
+apply eq_sym, (nat_add_sub_equiv_l Hn), (dim_is_unique Hnr).
 destruct Hnk as [Bk [HBk1 HBk2]].
 move: (is_generator_inclF HBk1) => /(inclF_monot_r _ _ _ (KerS_incl PE f)) HBk3.
 assert (HBk4 : mapF f Bk = 0)
@@ -2873,7 +2873,7 @@ Definition dual_basis : '(E -> R)^n := fun i x =>
   match (excluded_middle_informative (PE x)) with
   | left Hx (* in PE *) =>
       let (L, _) :=
-        span_EX _ _ (eq_ind_r (@^~ x) Hx (sym_eq (proj1 HB))) in
+        span_EX _ _ (eq_ind_r (@^~ x) Hx (eq_sym (proj1 HB))) in
       L i
   | right _ (* not in PE *) => 0
   end.
@@ -2939,9 +2939,9 @@ Proof.
 intros i.
 split.
 intros x y Hx Hy.
-generalize (eq_ind_r (@^~ x) Hx (sym_eq (proj1 HB)));
+generalize (eq_ind_r (@^~ x) Hx (eq_sym (proj1 HB)));
     intros Y; inversion Y as [Lx HLx]; clear Y.
-generalize (eq_ind_r (@^~ y) Hy (sym_eq (proj1 HB)));
+generalize (eq_ind_r (@^~ y) Hy (eq_sym (proj1 HB)));
     intros Y; inversion Y as [Ly HLy]; clear Y.
 erewrite dual_basis_correct.
 2: rewrite -comb_lin_plus_l; easy.
@@ -2950,7 +2950,7 @@ erewrite dual_basis_correct; try easy.
 (* *)
 intros x l.
 case (classic (PE x)); intros Hx.
-generalize (eq_ind_r (@^~ x) Hx (sym_eq (proj1 HB)));
+generalize (eq_ind_r (@^~ x) Hx (eq_sym (proj1 HB)));
     intros Y; inversion Y as [L HL].
 rewrite -> dual_basis_correct with (scal l (comb_lin L B)) (scal l L) i.
 rewrite -> dual_basis_correct with (comb_lin L B) L i; try easy.
@@ -2963,7 +2963,7 @@ rewrite Hl; replace 0 with (@zero R_Ring) by easy.
 rewrite scal_zero_l.
 eapply trans_eq.
 apply dual_basis_correct.
-apply sym_eq, comb_lin_zero_compat_l; try easy.
+apply eq_sym, comb_lin_zero_compat_l; try easy.
 easy.
 apply dual_basis_out.
 intros T.
@@ -2980,14 +2980,14 @@ Qed.
    facile à utiliser ????? *)
 (*Definition dual_basis2 : '(@Sg E PE -> R)^n := fun i x =>
    let (L,_) :=
-      (span_EX _ _ (eq_ind_r (@^~ (val x)) (val_in_P x) (sym_eq (proj1 HB)))) in
+      (span_EX _ _ (eq_ind_r (@^~ (val x)) (val_in_P x) (eq_sym (proj1 HB)))) in
          L i.*)
 
 Let HPE := is_basis_compatible_ms _ HB.
 
 Definition dual_basis2 : '(sub_ms HPE -> R)^n := fun i x =>
    let (L,_) :=
-      (span_EX _ _ (eq_ind_r (@^~ (val x)) (in_sub x) (sym_eq (proj1 HB)))) in
+      (span_EX _ _ (eq_ind_r (@^~ (val x)) (in_sub x) (eq_sym (proj1 HB)))) in
          L i.
 
 Lemma dual_basis2_correct : forall x L,
@@ -3363,7 +3363,7 @@ Context {E : AffineSpace V}.
 Lemma aff_span_compatible_as :
   forall {n} (A : 'E^n), compatible_as (aff_span A).
 Proof.
-intros; apply compatible_as_equiv, sym_eq; rewrite aff_span_eq.
+intros; apply compatible_as_equiv, eq_sym; rewrite aff_span_eq.
 apply barycenter_closure_idem_R.
 Qed.
 
@@ -3641,8 +3641,8 @@ Lemma aff_dim_lin_eq :
   forall {PE : E -> Prop} {O}, PE O -> aff_dim PE = dim (vectP PE O).
 Proof.
 intros PE O HO; unfold aff_dim; destruct (LPO _ _) as [[n Hn] | H]; simpl.
-apply sym_eq, dim_correct_l, has_aff_dim_lin; easy.
-apply sym_eq, dim_correct_r; intros n Hn; specialize (H n).
+apply eq_sym, dim_correct_l, has_aff_dim_lin; easy.
+apply eq_sym, dim_correct_r; intros n Hn; specialize (H n).
 contradict H; apply has_aff_dim_lin_rev in Hn; easy.
 Qed.*)
 
@@ -3793,7 +3793,7 @@ rewrite sum_nil in HL1; contradict HL1; apply not_eq_sym, one_not_zero_R.
 assert (HL1' : invertible (sum L)).
   rewrite HL1; replace 1 with (@one R_Ring); try easy; apply invertible_one.
 apply aff_span_ex; exists L; split; try easy.
-rewrite HL2; apply sym_eq, barycenter_ms_eq; easy.
+rewrite HL2; apply eq_sym, barycenter_ms_eq; easy.
 (* *)
 intros x; assert (Hx : aff_span A x) by now rewrite -HA.
 induction Hx as [L HL].
diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index 9603b4d6..3d992431 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -379,8 +379,8 @@ Definition maskPF {n} (P : 'Prop^n) (A : 'E^n) (x0 : E) : 'E^n :=
     end.
 
 Definition castF {n1 n2} (H : n1 = n2) (A : 'E^n1) : 'E^n2 :=
-  fun i2 => A (cast_ord (sym_eq H) i2).
-(* could be funF (cast_ord (sym_eq H)) A. *)
+  fun i2 => A (cast_ord (eq_sym H) i2).
+(* could be funF (cast_ord (eq_sym H)) A. *)
 
 Definition castF_p1S {n} (A : 'E^(n + 1)) : 'E^n.+1 := castF (addn1 n) A.
 Definition castF_Sp1 {n} (A : 'E^n.+1) : 'E^(n + 1) := castF (addn1_sym n) A.
@@ -389,17 +389,17 @@ Definition castF_1pS {n} (A : 'E^(1 + n)) : 'E^n.+1 := castF (add1n n) A.
 Definition castF_S1p {n} (A : 'E^n.+1) : 'E^(1 + n) := castF (add1n_sym n) A.
 
 Definition castF_ipn {n} (i0 : 'I_n.+1) (A : 'E^(i0 + (n - i0))) : 'E^n :=
-  castF (sym_eq (ord_split i0)) A.
+  castF (eq_sym (ord_split i0)) A.
 Definition castF_nip {n} (A : 'E^n) (i0 : 'I_n.+1) : 'E^(i0 + (n - i0)) :=
   castF (ord_split i0) A.
 
 Definition castF_ipS {n} (i0 : 'I_n.+1) (A : 'E^(i0 + (n - i0).+1)) : 'E^n.+1 :=
-  castF (sym_eq (ord_splitS i0)) A.
+  castF (eq_sym (ord_splitS i0)) A.
 Definition castF_Sip {n} (A : 'E^n.+1) (i0 : 'I_n.+1) : 'E^(i0 + (n - i0).+1) :=
   castF (ord_splitS i0) A.
 
 Definition castF_SpS {n} (i0 : 'I_n.+1) (A : 'E^(i0.+1 + (n - i0))) : 'E^n.+1 :=
-  castF (sym_eq (ordS_splitS i0)) A.
+  castF (eq_sym (ordS_splitS i0)) A.
 Definition castF_SSp {n} (A : 'E^n.+1) (i0 : 'I_n.+1) : 'E^(i0.+1 + (n - i0)) :=
   castF (ordS_splitS i0) A.
 
@@ -1382,19 +1382,19 @@ Lemma castF_inj :
   forall {n1 n2} (H : n1 = n2) (A1 B1 : 'E^n1),
     castF H A1 = castF H B1 -> A1 = B1.
 Proof.
-intros n1 n2 H A1 B1; rewrite -{2}(castF_id H (sym_eq H) A1)
-    -{2}(castF_id H (sym_eq H) B1).
+intros n1 n2 H A1 B1; rewrite -{2}(castF_id H (eq_sym H) A1)
+    -{2}(castF_id H (eq_sym H) B1).
 apply castF_eq_r.
 Qed.
 
 Lemma castF_can_l :
   forall {n1 n2} (H : n1 = n2),
-    cancel  (castF (sym_eq H)) (fun A1 : 'E^n1 => castF H A1).
+    cancel  (castF (eq_sym H)) (fun A1 : 'E^n1 => castF H A1).
 Proof. move=>>; rewrite castF_comp castF_refl; easy. Qed.
 
 Lemma castF_can_r :
   forall {n1 n2} (H : n1 = n2),
-    cancel (fun A1 : 'E^n1 => castF H A1) (castF (sym_eq H)).
+    cancel (fun A1 : 'E^n1 => castF H A1) (castF (eq_sym H)).
 Proof. move=>>; rewrite castF_comp castF_refl; easy. Qed.
 
 Lemma castF_cast_ord :
@@ -1435,7 +1435,7 @@ Proof.
 intros m1 m2 n Hm Am An; split; intros HA i.
 destruct (HA (cast_ord Hm i)) as [j Hj];
     rewrite castF_cast_ord in Hj; exists j; easy.
-destruct (HA (cast_ord (sym_eq Hm) i)) as [j Hj]; exists j; easy.
+destruct (HA (cast_ord (eq_sym Hm) i)) as [j Hj]; exists j; easy.
 Qed.
 
 Lemma invalF_castF_r_equiv :
@@ -1443,7 +1443,7 @@ Lemma invalF_castF_r_equiv :
     invalF Am (castF Hn An) <-> invalF Am An.
 Proof.
 intros m n1 n2 Hn Am An; split; intros HA i; destruct (HA i) as [j Hj].
-exists (cast_ord (sym_eq Hn) j); easy.
+exists (cast_ord (eq_sym Hn) j); easy.
 exists (cast_ord Hn j); rewrite castF_cast_ord; easy.
 Qed.
 
@@ -1454,7 +1454,7 @@ Proof. intros; rewrite invalF_castF_l_equiv invalF_castF_r_equiv; easy. Qed.
 
 Lemma invalF_castF_l :
   forall {n1 n2} (H : n1 = n2) (A1 : 'E^n1), invalF (castF H A1) A1.
-Proof. intros n1 n2 H A1 i2; exists (cast_ord (sym_eq H) i2); easy. Qed.
+Proof. intros n1 n2 H A1 i2; exists (cast_ord (eq_sym H) i2); easy. Qed.
 
 Lemma invalF_castF_r :
   forall {n1 n2} (H : n1 = n2) (A1 : 'E^n1), invalF A1 (castF H A1).
@@ -1465,9 +1465,9 @@ Qed.
 
 Lemma castF_sym_equiv :
   forall {n1 n2} (H : n1 = n2) (A1 : 'E^n1) (A2 : 'E^n2),
-    castF H A1 = A2 <-> castF (sym_eq H) A2 = A1.
+    castF H A1 = A2 <-> castF (eq_sym H) A2 = A1.
 Proof.
-intros n1 n2 H A1 A2; rewrite -{2}(castF_id H (sym_eq H) A1); split.
+intros n1 n2 H A1 A2; rewrite -{2}(castF_id H (eq_sym H) A1); split.
 intros; subst; easy.
 move=> /castF_inj; easy.
 Qed.
@@ -1754,7 +1754,7 @@ Lemma extendPF_funF_neqF_equiv :
 Proof.
 move=>> Hf; rewrite (extendPF_funF_equiv Hf).
 assert (H : forall P Q : Prop, P -> P /\ Q <-> Q) by tauto.
-apply H, sym_eq, funF_neqF.
+apply H, eq_sym, funF_neqF.
 Qed.
 
 Lemma extendPF_unfunF :
@@ -1790,7 +1790,7 @@ Lemma extendPF_unfunF_neqF :
     injective f ->
     extendPF f (neqF A1 x0) (neqF (unfunF f A1 x0) x0).
 Proof.
-move=>> Hf; apply (extendPF_unfunF_equiv Hf), sym_eq, (unfunF_neqF Hf).
+move=>> Hf; apply (extendPF_unfunF_equiv Hf), eq_sym, (unfunF_neqF Hf).
 Qed.
 
 Lemma extendPF_permutF :
@@ -2200,7 +2200,7 @@ Qed.
 
 Lemma firstF2 :
   forall {n1 n2 n3} (A : 'E^((n1 + n2) + n3)),
-    firstF (firstF A) = firstF (castF (sym_eq (addnA n1 n2 n3)) A).
+    firstF (firstF A) = firstF (castF (eq_sym (addnA n1 n2 n3)) A).
 Proof.
 intros; apply extF; intro; unfold firstF, castF; f_equal; apply ord_inj; easy.
 Qed.
@@ -2641,7 +2641,7 @@ intros K1.
 rewrite concatF_correct_r; try easy.
 f_equal; apply ord_inj; simpl.
 repeat rewrite -minusE.
-apply sym_eq, Nat.sub_add_distr.
+apply eq_sym, Nat.sub_add_distr.
 Qed.
 
 Lemma concatF_assoc_l :
@@ -2846,7 +2846,7 @@ Proof.
 intros; unfold castF_1pS; rewrite castF_refl.
 apply extF; intros i; destruct (ord_eq_dec i ord0) as [Hi | Hi].
 rewrite Hi insertF_correct_l// concatF_correct_l; easy.
-assert (Hi' : ~ (cast_ord (sym_eq (add1n n)) i < 1)%coq_nat)
+assert (Hi' : ~ (cast_ord (eq_sym (add1n n)) i < 1)%coq_nat)
     by now rewrite cast_ord_id; apply ord_n0_equiv_alt.
 rewrite insertF_correct_r insert_concat_r_ord_0 concatF_correct_r.
 f_equal; apply ord_inj; easy.
@@ -2859,7 +2859,7 @@ Proof.
 intros n A x0; unfold castF_p1S, castF.
 apply extF; intros i; destruct (ord_eq_dec i ord_max) as [Hi | Hi].
 rewrite Hi insertF_correct_l// concatF_correct_r singleF_0; easy.
-assert (Hi' : (cast_ord (sym_eq (addn1 n)) i < n)%coq_nat)
+assert (Hi' : (cast_ord (eq_sym (addn1 n)) i < n)%coq_nat)
     by now apply ord_nmax_equiv_alt.
 rewrite insertF_correct_r insert_concat_l_ord_max concatF_correct_l; easy.
 Qed.
@@ -2897,7 +2897,7 @@ Qed.
 
 Lemma insertF_concatF_r :
   forall {n1 n2} (A1 : 'E^n1) (A2 : 'E^n2) x0 {i0 : 'I_(n1 + n2).+1}
-      (H : ~ (cast_ord (sym_eq (addnS n1 n2)) i0 < n1)%coq_nat),
+      (H : ~ (cast_ord (eq_sym (addnS n1 n2)) i0 < n1)%coq_nat),
     insertF (concatF A1 A2) x0 i0 =
       castF (addnS n1 n2) (concatF A1 (insertF A2 x0 (concat_r_ord H))).
 Proof.
@@ -2908,7 +2908,7 @@ assert (H0 : (i < i0)%coq_nat) by (simpl in H; auto with zarith).
 rewrite insertF_correct_rl 2!concatF_correct_l; f_equal; apply ord_inj; easy.
 (* *)
 rewrite concatF_correct_r.
-destruct (nat_lt_eq_gt_dec i (cast_ord (sym_eq (addnS _ _)) i0))
+destruct (nat_lt_eq_gt_dec i (cast_ord (eq_sym (addnS _ _)) i0))
     as [[Hi0 | Hi0] | Hi0].
 (* . *)
 rewrite 2!insertF_correct_rl;
@@ -3396,7 +3396,7 @@ Lemma skip2F_compat_gen :
 Proof.
 intros n A B i0 i1 j0 j1 Hi Hj H Hi0 Hi1; subst j0 j1.
 destruct (nat_lt_eq_gt_dec i1 i0) as [[Hia | Hia] | Hia].
-2: contradict Hi; apply ord_inj, sym_eq; easy.
+2: contradict Hi; apply ord_inj, eq_sym; easy.
 (* *)
 rewrite 2!(skip2F_sym _ (ord_lt_neq_sym Hia)).
 apply skip2F_compat_lt, eqx2F_sym_i; easy.
@@ -3935,9 +3935,9 @@ Qed.
 
 Lemma permutF_castF :
   forall {n1 n2} (H : n1 = n2) p (A1 : 'E^n1),
-    permutF p (castF H A1) = castF H (permutF (cast_f_ord (sym_eq H) p) A1).
+    permutF p (castF H A1) = castF H (permutF (cast_f_ord (eq_sym H) p) A1).
 Proof.
-intros; apply (castF_inj (sym_eq H)); rewrite castF_permutF !castF_can_r; easy.
+intros; apply (castF_inj (eq_sym H)); rewrite castF_permutF !castF_can_r; easy.
 Qed.
 
 Lemma permutF_liftF_S :
@@ -4095,9 +4095,9 @@ Lemma moveF_castF :
   forall {n1 n2} (H : n1 = n2) (A1 : 'E^n1.+1) i0 i1,
     let HH := eq_S n1 n2 H in
     moveF (castF HH A1) i0 i1 =
-      castF HH (moveF A1 (cast_ord (sym_eq HH) i0) (cast_ord (sym_eq HH) i1)).
+      castF HH (moveF A1 (cast_ord (eq_sym HH) i0) (cast_ord (eq_sym HH) i1)).
 Proof.
-intros n1 n2 H A1 i0 i1 HH; apply (castF_inj (sym_eq HH)).
+intros n1 n2 H A1 i0 i1 HH; apply (castF_inj (eq_sym HH)).
 rewrite castF_moveF !cast_ord_comp !cast_ord_id; easy.
 Qed.
 
@@ -4213,7 +4213,7 @@ Lemma last_f_extendF :
     exists (p : 'I_[n1 + n2]), bijective p /\ f = lastF p.
 Proof.
 intros n1 n2 f' Hf'; pose (f := revF f').
-assert (Hf0 : f' = revF f) by apply sym_eq, revF_invol.
+assert (Hf0 : f' = revF f) by apply eq_sym, revF_invol.
 assert (Hf1 : injective f) by now apply revF_inj_compat.
 destruct (injF_extend_bij_EX Hf1) as [p [Hp1 Hp2]]; exists (revF p).
 split; [apply injF_bij, revF_inj_compat, bij_inj; easy |].
@@ -4757,7 +4757,7 @@ Aglopted.
 Lemma filter_neqF_concatF_l :
   forall {n1 n2} (A1 : 'E^n1) {A2 : 'E^n2} {x0} (HA2 : A2 = constF n2 x0),
     filter_neqF (concatF A1 A2) x0 =
-      castF (sym_eq (len_neqF_concatF_l A1 HA2)) (filter_neqF A1 x0).
+      castF (eq_sym (len_neqF_concatF_l A1 HA2)) (filter_neqF A1 x0).
 Proof.
 Aglopted.
 
@@ -4770,7 +4770,7 @@ Aglopted.
 Lemma filter_neqF_concatF_r :
   forall {n1 n2} {A1 : 'E^n1} {x0} (HA1 : A1 = constF n1 x0) (A2 : 'E^n2),
     filter_neqF (concatF A1 A2) x0 =
-      castF (sym_eq (len_neqF_concatF_r HA1 A2)) (filter_neqF A2 x0).
+      castF (eq_sym (len_neqF_concatF_r HA1 A2)) (filter_neqF A2 x0).
 Proof.
 Aglopted.*)
 
@@ -4827,9 +4827,9 @@ Lemma lenPF_extendPF :
     injective f -> extendPF f P1 P2 -> lenPF P1 = lenPF P2.
 Proof.
 intros n1 n2 f P1 P2 Hf HP.
-pose (Hn := sym_eq (subnKC (injF_leq Hf))).
+pose (Hn := eq_sym (subnKC (injF_leq Hf))).
 pose (g i1 := cast_ord Hn (f i1)).
-assert (Hg1 : forall i1, f i1 = cast_ord (sym_eq Hn) (g i1))
+assert (Hg1 : forall i1, f i1 = cast_ord (eq_sym Hn) (g i1))
     by now intros; rewrite cast_ord_comp cast_ord_id.
 assert (Hg2 : injective g) by now unfold g; move=>> /cast_ord_inj /Hf.
 destruct (first_f_extendF Hg2) as [p [Hp Hp1]]; move: Hp => /bij_inj Hp2.
@@ -4839,7 +4839,7 @@ apply lenPF_ext; intros i1; destruct (HP (f i1)) as [[j1 [Hj1 Hj2]] | [H _]];
     [| exfalso; rewrite Rg_compl in H; apply (H i1); easy].
 apply Hf in Hj1; subst; rewrite Hj2 Hg1 Hp1 firstF_permutF; easy.
 (* *)
-intros j; destruct (HP (cast_ord (sym_eq Hn) (p (last_ord n1 j))))
+intros j; destruct (HP (cast_ord (eq_sym Hn) (p (last_ord n1 j))))
     as [[j1 [Hj _]] | [_ H]]; [exfalso | easy].
 rewrite Hg1 Hp1 in Hj; apply cast_ord_inj, Hp2, ord_compat in Hj.
 destruct j1 as [j1 Hj1]; simpl in Hj.
@@ -4887,7 +4887,7 @@ apply subset_ext_equiv; split; intros i2 HP2;
     [| inversion HP2; apply filterP_ord_correct].
 destruct (im_dec f i2) as [[i1 <-] | Hi2].
 (* *)
-apply Rg_ex; exists (cast_ord (sym_eq H) (unfilterP_ord HP2 (f i1))).
+apply Rg_ex; exists (cast_ord (eq_sym H) (unfilterP_ord HP2 (f i1))).
 rewrite cast_ord_comp cast_ord_id filterP_unfilterP_ord_in; easy.
 (* *)
 contradict Hi2; rewrite not_all_not_ex_equiv.
diff --git a/FEM/Algebra/ModuleSpace_compl.v b/FEM/Algebra/ModuleSpace_compl.v
index fec3c54e..3f5afbda 100644
--- a/FEM/Algebra/ModuleSpace_compl.v
+++ b/FEM/Algebra/ModuleSpace_compl.v
@@ -130,7 +130,7 @@ Lemma convex_comb_2_eq :
   forall a1 a2 (u1 u2 : E),
     a1 + a2 = 1 -> scal a1 u1 + scal a2 u2 = scal a1 (u1 - u2) + u2.
 Proof.
-move=>> Ha; apply sym_eq in Ha; rewrite plus_minus_r_equiv in Ha; subst.
+move=>> Ha; apply eq_sym in Ha; rewrite plus_minus_r_equiv in Ha; subst.
 rewrite scal_minus_l scal_one minus_sym scal_minus_r plus_assoc; easy.
 Qed.
 
@@ -499,7 +499,7 @@ Proof. intros; subst; easy. Qed.
 Lemma scalF_castF :
   forall {n1 n2} (H : n1 = n2) a1 (u1 : 'E^n1),
     scalF (castF H a1) (castF H u1) = castF H (scalF a1 u1).
-Proof. intros; apply sym_eq, scalF_castF_compat; easy. Qed.
+Proof. intros; apply eq_sym, scalF_castF_compat; easy. Qed.
 
 Lemma scalF_firstF :
   forall {n1 n2} a (u : 'E^(n1 + n2)),
@@ -938,14 +938,14 @@ Qed.
 Lemma comb_lin_castF :
   forall {n1 n2} (H : n1 = n2) L (B : 'E^n1),
     comb_lin (castF H L) (castF H B) = comb_lin L B.
-Proof. intros n1 n2 H L B; apply sym_eq, (comb_lin_castF_compat H); easy. Qed.
+Proof. intros n1 n2 H L B; apply eq_sym, (comb_lin_castF_compat H); easy. Qed.
 
 Lemma comb_lin_castF_l :
   forall {n1 n2} (H : n1 = n2) L1 (B2 : 'E^n2),
     comb_lin (castF H L1) B2 = comb_lin L1 (castF (eq_sym H) B2).
 Proof.
 intros n1 n2 H L1 B2.
-apply sym_eq, (comb_lin_castF_compat H); try rewrite castF_id; easy.
+apply eq_sym, (comb_lin_castF_compat H); try rewrite castF_id; easy.
 Qed.
 
 Lemma comb_lin_castF_r :
@@ -953,7 +953,7 @@ Lemma comb_lin_castF_r :
     comb_lin L2 (castF H B1) = comb_lin (castF (eq_sym H) L2) B1.
 Proof.
 intros n1 n2 H L2 B1.
-apply sym_eq, (comb_lin_castF_compat H); try rewrite castF_id; easy.
+apply eq_sym, (comb_lin_castF_compat H); try rewrite castF_id; easy.
 Qed.
 
 Lemma comb_lin_zero_l : forall {n} (B : 'E^n), comb_lin 0 B = 0.
@@ -1441,7 +1441,7 @@ Lemma scal_comb_lin_l :
     scal (comb_lin L L') B = comb_lin L (scalF L' (constF n B)).
 Proof.
 intros n L L' B; induction n.
-rewrite comb_lin_nil scal_zero_l; apply sym_eq, comb_lin_nil.
+rewrite comb_lin_nil scal_zero_l; apply eq_sym, comb_lin_nil.
 rewrite !comb_lin_ind_l scal_distr_r IHn; f_equal.
 rewrite scal_assoc; easy.
 Qed.
@@ -1709,7 +1709,7 @@ intros n1 n2 L1 B1 B2 HB H2 L2.
 induction n1.
 (* *)
 rewrite comb_lin_nil.
-apply sym_eq, comb_lin_zero_compat_l, extF; intro.
+apply eq_sym, comb_lin_zero_compat_l, extF; intro.
 rewrite zeroF; unfold L2; rewrite comb_lin_zero_compat_l; try easy.
 apply extF; intros [i1 Hi1].
 contradict Hi1; auto with arith.
@@ -1738,9 +1738,9 @@ rewrite -> scal_zero_compat_l, plus_zero_l.
 apply comb_lin_eq_l, extF; intros i1.
 case (charac_or (fun i0 : 'I_n1 => B1 (lift_S i0) = B2 i2) i1); intros H.
 rewrite H; apply charac_out_equiv in H.
-apply sym_eq, charac_is_0; easy.
+apply eq_sym, charac_is_0; easy.
 rewrite H; apply (charac_in_equiv _ i1) in H.
-apply sym_eq, charac_is_1; easy.
+apply eq_sym, charac_is_1; easy.
 apply charac_is_0.
 intros HK.
 apply Hi2; f_equal; apply H2.
@@ -1762,7 +1762,7 @@ intros n1 n2 L1 B1 B2 HB H2 L2.
 induction n1.
 (* *)
 rewrite comb_lin_nil; split.
-apply sym_eq, comb_lin_zero_compat_l, extF; intros i2.
+apply eq_sym, comb_lin_zero_compat_l, extF; intros i2.
 unfold L2; rewrite comb_lin_zero_compat_l.
 rewrite scal_zero_r; easy.
 apply extF; intros i1.
diff --git a/FEM/Algebra/Monoid_compl.v b/FEM/Algebra/Monoid_compl.v
index ee6ffdda..4ba06af1 100644
--- a/FEM/Algebra/Monoid_compl.v
+++ b/FEM/Algebra/Monoid_compl.v
@@ -572,7 +572,7 @@ Proof. move=>>; apply len_neqF_concatF_l. Qed.
 Lemma filter_n0F_concatF_l :
   forall {n1 n2} (u1 : 'G^n1) {u2 : 'G^n2} (Hu2 : u2 = 0),
     filter_n0F (concatF u1 u2) =
-      castF (sym_eq (len_n0F_concatF_l u1 Hu2)) (filter_n0F u1).
+      castF (eq_sym (len_n0F_concatF_l u1 Hu2)) (filter_n0F u1).
 Proof.
 intros; unfold filter_n0F; rewrite filter_neqF_concatF_l; apply castF_eq_l.
 Qed.
@@ -585,7 +585,7 @@ Proof. move=>>; apply len_neqF_concatF_r. Qed.
 Lemma filter_n0F_concatF_r :
   forall {n1 n2} {u1 : 'G^n1} (Hu1 : u1 = 0) (u2 : 'G^n2),
     filter_n0F (concatF u1 u2) =
-      castF (sym_eq (len_n0F_concatF_r Hu1 u2)) (filter_n0F u2).
+      castF (eq_sym (len_n0F_concatF_r Hu1 u2)) (filter_n0F u2).
 Proof.
 intros; unfold filter_n0F; rewrite filter_neqF_concatF_r; apply castF_eq_l.
 Qed.*)
@@ -1876,7 +1876,7 @@ Proof. intros; subst; apply sum_ext; intros; rewrite castF_refl; easy. Qed.
 Lemma sum_castF :
   forall {n1 n2} (H : n1 = n2) (u : 'G^n1),
     sum (castF H u) = sum u.
-Proof. intros; eapply sym_eq, (sum_castF_compat); easy. Qed.
+Proof. intros; eapply eq_sym, (sum_castF_compat); easy. Qed.
 
 Lemma sum_zero : forall {n}, sum (0 : 'G^n) = 0.
 Proof. intros; apply sum_zero_compat; easy. Qed.
@@ -2554,7 +2554,7 @@ Qed.
 Lemma concatnF_ind_l :
   forall {n} {b : 'nat^n.+1} (g : forall i, 'G^(b i)),
     concatnF g
-      = castF (sym_eq (sum_ind_l b))
+      = castF (eq_sym (sum_ind_l b))
               (concatF (g ord0) (concatnF (fun i => (g (lift_S i) )))).
 Proof.
 intros n b g.
@@ -2573,7 +2573,7 @@ Qed.
 Lemma concatnF_ind_r :
   forall {n} {b : 'nat^n.+1} (g : forall i, 'G^(b i)),
     concatnF g
-      = castF (sym_eq (sum_ind_r b))
+      = castF (eq_sym (sum_ind_r b))
               (concatF (concatnF (fun i => g (widen_S i))) (g ord_max)).
 Proof.
 intros n b g.
@@ -3008,7 +3008,7 @@ Lemma concatnF_invalF :
 Proof.
 intros n b g i j.
 exists (concatn_ord b i j).
-apply sym_eq, concatn_ord_correct.
+apply eq_sym, concatn_ord_correct.
 Qed.
 
 Lemma concatnF_inclF_equiv :
@@ -3188,8 +3188,8 @@ Proof.
 intros Q n b g Htrans H1 H2.
 apply (sortedF_castF_equiv (sum_is_S b)), sortedF_equiv; [easy |].
 intros i Hi; unfold castF.
-pose (i' := cast_ord (sym_eq (sum_is_S b)) i).
-pose (j' := cast_ord (sym_eq (sum_is_S b)) (Ordinal Hi)).
+pose (i' := cast_ord (eq_sym (sum_is_S b)) i).
+pose (j' := cast_ord (eq_sym (sum_is_S b)) (Ordinal Hi)).
 assert (Q (concatnF g i') (concatnF g j')); try easy.
 destruct (splitn_ord1_S i' j') as [[K1 K2] | [K1 [K2 K3]]]; [easy |..].
 (* *)
diff --git a/FEM/Algebra/Ring_compl.v b/FEM/Algebra/Ring_compl.v
index dd6d55e0..2339d01c 100644
--- a/FEM/Algebra/Ring_compl.v
+++ b/FEM/Algebra/Ring_compl.v
@@ -113,7 +113,7 @@ Lemma inv_correct_rev :
   forall {x y}, invertible x -> y = inv x -> is_inverse x y.
 Proof.
 move=>> [y' Hy'] Hy; rewrite Hy; apply (is_inverse_compat_r  y'); try easy.
-apply sym_eq, inv_correct; easy.
+apply eq_sym, inv_correct; easy.
 Qed.
 
 End Ring_Def1.
diff --git a/FEM/Algebra/nat_compl.v b/FEM/Algebra/nat_compl.v
index c7dcddc7..44e7fa43 100644
--- a/FEM/Algebra/nat_compl.v
+++ b/FEM/Algebra/nat_compl.v
@@ -395,10 +395,10 @@ Lemma add1n_sym : forall n, n.+1 = 1 + n.
 Proof. easy. Qed.
 
 Lemma addSn_sym : forall m n, (m + n).+1 = m.+1 + n.
-Proof. intros; apply sym_eq, addSn. Qed.
+Proof. intros; apply eq_sym, addSn. Qed.
 
 Lemma addnS_sym : forall m n, (m + n).+1 = m + n.+1.
-Proof. intros; apply sym_eq, addnS. Qed.
+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.
diff --git a/FEM/Compl/Function_compl.v b/FEM/Compl/Function_compl.v
index ef9ffb5d..0939070f 100644
--- a/FEM/Compl/Function_compl.v
+++ b/FEM/Compl/Function_compl.v
@@ -493,7 +493,7 @@ Context {f : T1 -> T2}.
 Hypothesis Hf : bijective f.
 
 Lemma f_inv_invol : forall (Hf1 : bijective (f_inv Hf)), f_inv Hf1 = f.
-Proof. intros; apply sym_eq, f_inv_uniq_l, f_inv_correct_r. Qed.
+Proof. intros; apply eq_sym, f_inv_uniq_l, f_inv_correct_r. Qed.
 
 Lemma f_inv_invol_alt : f_inv (f_inv_bij Hf) = f.
 Proof. apply f_inv_invol. Qed.
diff --git a/FEM/Compl/Function_sub.v b/FEM/Compl/Function_sub.v
index 428b98e9..414a232e 100644
--- a/FEM/Compl/Function_sub.v
+++ b/FEM/Compl/Function_sub.v
@@ -101,7 +101,7 @@ Context {P2 : T2 -> Prop}.
 Context {f : T1 -> T2}.
 
 Lemma RgS_eq : RgS P1 f = RgS_gen P1 (RgS P1 f) f.
-Proof. apply sym_eq, inter_idem. Qed.
+Proof. apply eq_sym, inter_idem. Qed.
 
 Lemma RgS_correct : forall {x2} x1, P1 x1 -> f x1 = x2 -> RgS P1 f x2.
 Proof. intros; subst; easy. Qed.
-- 
GitLab