diff --git a/FEM/Algebra/Sub_struct.v b/FEM/Algebra/Sub_struct.v
index 5c5ecc3d8d2b1f44bc26d6388081add2d7828f63..284e51e487cdd18fcb0f70b96645541fb9d26d74 100644
--- a/FEM/Algebra/Sub_struct.v
+++ b/FEM/Algebra/Sub_struct.v
@@ -36,7 +36,7 @@ From FEM Require Import AffineSpace.
  the ring of real numbers R_Ring. *)
 
 
-Section Sub_Algebraic_Structure.
+Section Sub_Algebraic_Structure1.
 
 Context {T : Type}.
 Context {compatible : (T -> Prop) -> Prop}.
@@ -52,24 +52,14 @@ Definition mk_sub {x : T} (Hx : PT x) : sub_struct HPT := mk_sub_ HPT x Hx.
 Definition val (x : sub_struct HPT) : T := val_ HPT x.
 Definition in_sub (x : sub_struct HPT) : PT x := in_sub_ HPT x.
 
-Lemma val_eq : forall (x y : sub_struct HPT), x = y -> val x = val y.
+Lemma val_eq : forall {x y : sub_struct HPT}, x = y -> val x = val y.
 Proof. apply f_equal. Qed.
 
-Lemma val_inj : forall (x y : sub_struct HPT), val x = val y -> x = y.
+Lemma val_inj : forall {x y : sub_struct HPT}, val x = val y -> x = y.
 Proof.
 intros [x Hx] [y Hy]; simpl; intros; subst; f_equal; apply proof_irrel.
 Qed.
 
-Lemma mk_sub_eq :
-  forall (x y : T) (Hx : PT x) (Hy : PT y),
-    x = y -> mk_sub Hx = mk_sub Hy.
-Proof. intros; apply val_inj; easy. Qed.
-
-Lemma mk_sub_inj :
-  forall (x y : T) (Hx : PT x) (Hy : PT y),
-    mk_sub Hx = mk_sub Hy -> x = y.
-Proof. move=>>; apply val_eq. Qed.
-
 Lemma sub_struct_inhabited : inhabited (sub_struct HPT) <-> nonempty PT.
 Proof.
 split. intros [x]; exists (val x); apply in_sub.
@@ -81,7 +71,27 @@ Lemma val_inclF_compat :
     inclF A QT -> inclF (fun i => val (A i)) PT.
 Proof. intros QT n A HA i; specialize (HA i); destruct (A i); easy. Qed.
 
-End Sub_Algebraic_Structure.
+End Sub_Algebraic_Structure1.
+
+
+Section Sub_Algebraic_Structure2.
+
+Context {T : Type}.
+Context {compatible : (T -> Prop) -> Prop}.
+Context {PT : T -> Prop}.
+Hypothesis HPT : compatible PT.
+
+Lemma mk_sub_eq :
+  forall {x y : T} (Hx : PT x) (Hy : PT y),
+    x = y -> mk_sub Hx = mk_sub Hy :> sub_struct HPT.
+Proof. intros; apply val_inj; easy. Qed.
+
+Lemma mk_sub_inj :
+  forall {x y : T} (Hx : PT x) (Hy : PT y),
+    mk_sub Hx = mk_sub Hy :> sub_struct HPT -> x = y.
+Proof. move=>> /val_eq; easy. Qed.
+
+End Sub_Algebraic_Structure2.
 
 
 Section Span_Algebraic_Structure.
@@ -129,6 +139,10 @@ Context {f : T1 -> T2}.
 Context {fS : sub_struct HP1 -> sub_struct HP2}.
 Hypothesis HfS : forall x1, val (fS x1) = f (val x1).
 
+Lemma sub_fun_rev : funS P1 P2 f.
+Proof.
+Admitted.
+
 Lemma sub_inj : injS P1 f -> injective fS.
 Proof.
 intros Hf; apply inj_S_equiv.
@@ -136,6 +150,15 @@ move=> [x1 Hx1] [y1 Hy1] _ _ /(f_equal val); rewrite !HfS; simpl.
 move=> /(Hf _ _ Hx1 Hy1) H1; apply val_inj; simpl; easy.
 Qed.
 
+Lemma sub_inj_rev : injective fS -> injS P1 f.
+Proof.
+move=> /inj_S_equiv Hf x1 y1 Hx1 Hy1 H1.
+apply (mk_sub_inj HP1 Hx1 Hy1), Hf; [..| apply val_inj; rewrite !HfS]; easy.
+Qed.
+
+Lemma sub_inj_equiv : injS P1 f <-> injective fS.
+Proof. split; [apply sub_inj | apply sub_inj_rev]. Qed.
+
 Lemma sub_surj : surjS P1 P2 f -> surjective fS.
 Proof.
 intros Hf; apply surj_S_equiv.
@@ -143,12 +166,31 @@ intros [x2 Hx2] _; destruct (Hf _ Hx2) as [x1 [Hx1a Hx1b]].
 exists (mk_sub Hx1a); split; [| apply val_inj; rewrite HfS]; easy.
 Qed.
 
+Lemma sub_surj_rev : surjective fS -> surjS P1 P2 f.
+Proof.
+move=> /surj_S_equiv Hf x2 Hx2;
+    destruct (Hf (mk_sub Hx2)) as [[x1 Hx1] [_ Hx1a]]; [easy |].
+exists x1; split; [| move: Hx1a => /(f_equal val); rewrite HfS]; easy.
+Qed.
+
+Lemma sub_surj_equiv : surjS P1 P2 f <-> surjective fS.
+Proof. split; [apply sub_surj | apply sub_surj_rev]. Qed.
+
 Lemma sub_bij : bijS P1 P2 f -> bijective fS.
 Proof.
-move=>> /(bijS_equiv HT1) [_ Hf];
+move=> /(bijS_equiv HT1) [_ Hf];
     apply bij_equiv; split; [apply sub_inj | apply sub_surj]; easy.
 Qed.
 
+Lemma sub_bij_rev : bijective fS -> bijS P1 P2 f.
+Proof.
+move=> /bij_equiv Hf; apply (bijS_equiv HT1); repeat split;
+    [apply sub_fun_rev | apply sub_inj_rev | apply sub_surj_rev]; easy.
+Qed.
+
+Lemma sub_bij_equiv : bijS P1 P2 f <-> bijective fS.
+Proof. split; [apply sub_bij | apply sub_bij_rev]. Qed.
+
 End Sub_Fct1.
 
 
@@ -2317,15 +2359,39 @@ Context {f : E1 -> E2}.
 Context {fS : sub_ms HPE1 -> sub_ms HPE2}.
 Hypothesis HfS : forall x, val (fS x) = f (val x).
 
+Lemma sub_ms_fun_rev : funS PE1 PE2 f.
+Proof.
+apply: (sub_fun_rev _ HPE1 HPE2).
+apply inhabited_ms.
+Admitted.
+
 Lemma sub_ms_inj : injS PE1 f -> injective fS.
 Proof. apply sub_inj; easy. Qed.
 
+Lemma sub_ms_inj_rev : injective fS -> injS PE1 f.
+Proof. apply sub_inj_rev; easy. Qed.
+
+Lemma sub_ms_inj_equiv : injS PE1 f <-> injective fS.
+Proof. apply sub_inj_equiv; easy. Qed.
+
 Lemma sub_ms_surj : surjS PE1 PE2 f -> surjective fS.
 Proof. apply sub_surj; easy. Qed.
 
+Lemma sub_ms_surj_rev : surjective fS -> surjS PE1 PE2 f.
+Proof. apply sub_surj_rev; easy. Qed.
+
+Lemma sub_ms_surj_equiv : surjS PE1 PE2 f <-> surjective fS.
+Proof. apply sub_surj_equiv; easy. Qed.
+
 Lemma sub_ms_bij : bijS PE1 PE2 f -> bijective fS.
 Proof. apply sub_bij; [apply inhabited_ms | easy]. Qed.
 
+Lemma sub_ms_bij_rev : bijective fS -> bijS PE1 PE2 f.
+Proof. apply sub_bij_rev; [apply inhabited_ms | easy]. Qed.
+
+Lemma sub_ms_bij_equiv : bijS PE1 PE2 f <-> bijective fS.
+Proof. apply sub_bij_equiv; [apply inhabited_ms | easy]. Qed.
+
 Lemma sub_ms_f_scal_compat : f_scal_compat f -> f_scal_compat fS.
 Proof. intros Hf a x1; apply val_inj; rewrite HfS Hf -!HfS; easy. Qed.
 
diff --git a/FEM/FE.v b/FEM/FE.v
index f67205b82dda94a4b6be8257b80d424dc0c5bbe3..e098da06bf9cdaf810fea3f3477dda1f419f490b 100644
--- a/FEM/FE.v
+++ b/FEM/FE.v
@@ -78,7 +78,7 @@ apply trans_eq with (val (mk_sub_ms_ PC Hp1)); try easy.
 rewrite (H2 (mk_sub_ms_ _ Hp1)); try easy.
 Qed.
 
-(* TODO Fc 19/02/24 : generaliser et deplacer dans Sub_struct.v *)
+(* TODO FC 19/02/24 : generaliser et deplacer dans Sub_struct.v *)
 Lemma bijS_equiv_sub_ms : forall sigma : FRd d-> 'R^n,
   is_linear_mapping sigma -> 
   bijS P fullset sigma
@@ -90,7 +90,7 @@ rewrite (lmS_bijS_injS_gen_equiv n P_has_dim n); try easy.
 apply sigma_injS_equiv; easy.
 Qed.
 
-(* TODO Fc 19/02/24 : generaliser et deplacer dans Sub_struct.v *)
+(* TODO FC 19/02/24 : generaliser et deplacer dans Sub_struct.v *)
 Lemma bijS_is_free : forall sigma : FRd d-> 'R^n,
   is_linear_mapping sigma ->
     bijS P fullset sigma -> is_free (scatter sigma).
diff --git a/FEM/P_approx_k.v b/FEM/P_approx_k.v
index fad3ea6bfa1828aed4a1968b3e181517e32c5afc..47a64641766d22ad40dcfb9d81e8f4b4e8bc57ed 100644
--- a/FEM/P_approx_k.v
+++ b/FEM/P_approx_k.v
@@ -948,17 +948,6 @@ unfold castF; rewrite concatF_correct_l; try easy.
 f_equal; apply ord_inj; now simpl.
 Qed.
 
-(* TODO SB bouger *)
-Lemma replaceF_switch :
-  forall {E : Type} {n : nat} (A : 'E^n) (x0 x1 : E) {i0 i1 : 'I_n},
-  i1 <> i0 -> replaceF (replaceF A x0 i0) x1 i1 = replaceF (replaceF A x1 i1) x0 i0.
-Proof.
-intros E n A x0 x1 i0 i1 H.
-rewrite -replace2F_equiv_def; try easy.
-now apply sym_not_eq.
-Qed.
-
-
 Lemma DeriveF_part_scal_fun : forall {n} i (alpha:'nat^n.+1) (Hi: i<>ord_max) (g1:R->R) (g2: 'R^n.+1 -> R),
   (forall (x:'R^n.+1) y, g2 x = g2 (replaceF x y ord_max)) ->
   DeriveF_part alpha i (fun x:'R^n.+1 => g1 (x ord_max) * g2 x)
@@ -1000,7 +989,8 @@ apply ord_inj; now simpl.
 unfold widenF_S; f_equal; apply ord_inj; now simpl.
 intros x y; unfold Derive_multii; f_equal.
 apply fun_ext; intros z.
-rewrite replaceF_switch; try easy.
+fold (replace2F x y z ord_max (Ordinal Hi')).
+rewrite replace2F_equiv_def; try easy.
 apply ord_neq; simpl; easy.
 rewrite replaceF_correct_r; try easy.
 apply ord_neq; simpl; easy.
@@ -1742,10 +1732,6 @@ rewrite P_approx_1_d_eq_ref.
 apply span_inclF_diag.
 Qed.
 
-(* TODO FC (23/02/2023): exprimer l'unisolvance directement sur les polynômes et les nœuds.
-Lemma P_approx_1_d_unisolvance : 
-*)
-
 Lemma P_approx_1_d_eq_cur : forall vtx_cur, 
   affine_independent vtx_cur ->
   P_approx_1_d d = span (LagP1_d_cur vtx_cur).