diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index 2bfd993d385cca67aad69db5b17695f8d9a2ea02..6feb6575c87cc6d4dbf7d13ea6c2e031863f6a76 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -4896,7 +4896,6 @@ rewrite (filterP_ord_Rg_aux2 Hf HP).
 apply filterP_ord_Rg_aux3.
 Qed.
 
-(* TODO FC (01/02/2024): try using PAF_ind_l. *)
 Lemma Rg_0_liftF_S :
   forall  {n1 n2} {f : 'I_{n1.+1,n2}},
     Rg f = union (eq^~ (f ord0)) (Rg (liftF_S f)).
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index b0f8b320b23d1924bce0581689f4123c6d8e9038..0e77f1b8a648aa444ae3eef8ccecd011d1e7d6cd 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -978,6 +978,25 @@ Proof. intros; apply ord_lt_neq, widen_lt_lift_S. Qed.
 Lemma lift_not_widen_S : forall {n} (i : 'I_n), lift_S i <> widen_S i.
 Proof. intros; apply not_eq_sym, widen_not_lift_S. Qed.
 
+Lemma widen_S_inj : forall {n}, injective (@widen_S n).
+Proof. intros; apply widen_ord_inj. Qed.
+
+Lemma narrow_S_inj :
+  forall {n} {i j : 'I_n.+1} (Hi : i <> ord_max) (Hj : j <> ord_max),
+    narrow_S Hi = narrow_S Hj -> i = j.
+Proof. move=>> /(f_equal widen_S); rewrite !widen_narrow_S; easy. Qed.
+
+Lemma lift_S_inj : forall {n}, injective (@lift_S n).
+Proof.
+intros n; replace (injective lift_S) with (injective (@lift_S n.+1.-1));
+    [apply lift_inj | easy].
+Qed.
+
+Lemma lower_S_inj :
+  forall {n} {i j : 'I_n.+1} (Hi : i <> ord0) (Hj : j <> ord0),
+    lower_S Hi = lower_S Hj -> i = j.
+Proof. move=>> /(f_equal lift_S); rewrite !lift_lower_S; easy. Qed.
+
 End Widen_Lift_S.
 
 
@@ -1042,14 +1061,12 @@ Lemma sortedF_S_sortedF :
 Proof.
 intros n A HT HA; apply (sortedF_S_sortedF_aux HT).
 apply (strong_induction (fun p => forall i H, leT (A i) (A (Ordinal H)))).
-intros p; destruct p as [|p].
+intros p; destruct p as [|p]; intros Hp i H1.
 (* *)
-intros Hp i H1.
 assert (H2 : i.+1 = i + 0 + 1) by now rewrite -addn0_sym addn1.
 assert (H3 : i.+1 < n) by now rewrite H2.
 replace (Ordinal _) with (Ordinal H3); [apply HA | apply ord_inj; easy].
 (* *)
-intros Hp i H1.
 assert (H2 : i + p + 1 < n)
     by now apply ltn_trans with (i + p.+1 + 1); [rewrite ltn_add2r ltn_add2l |].
 apply HT with (A (Ordinal H2)).
@@ -1341,7 +1358,7 @@ apply incrF_comp; [apply cast_ord_incrF | easy].
 apply Rg_ex; exists (cast_ord H1 i1); rewrite comp_correct cast_ordK; easy.
 Qed.
 
-(* Definition and properties of cast_f_ord. *)
+(** Definition and properties of cast_f_ord. *)
 
 Definition cast_f_ord {n1 n2} (H : n1 = n2) (p1 : 'I_[n1]) : 'I_[n2] :=
   fun i2 => cast_ord H (p1 (cast_ord (sym_eq H) i2)).
@@ -1617,7 +1634,7 @@ Lemma insert_concat_l_ord_max :
     insert_ord Hi1 = concat_l_ord Hi2.
 Proof. intros; rewrite insert_ord_correct_l; apply ord_inj; easy. Qed.
 
-(* Definition and properties of skip_f_ord. *)
+(** Definition and properties of skip_f_ord. *)
 
 Lemma skip_f_not :
   forall {n} {p : 'I_[n.+1]} (Hp : injective p) i0 j,
@@ -1684,7 +1701,7 @@ rewrite -{1}(f_inv_correct_r Hp i0) -skip_f_ord_comp_alt skip_f_ord_id//.
 apply f_inv_correct_l.
 Qed.
 
-(* Definition and properties of insert_f_ord. *)
+(** Definition and properties of insert_f_ord. *)
 
 Definition insert_f_ord {n} (p : 'I_[n]) i0 : 'I_[n.+1] :=
   fun i => match (ord_eq_dec i i0) with
@@ -1704,7 +1721,7 @@ intros; unfold insert_f_ord; destruct (ord_eq_dec _ _);
     [easy | repeat f_equal; apply proof_irrelevance].
 Qed.
 
-(* Definition and properties of extend_f_S. *)
+(** Definition and properties of extend_f_S. *)
 
 Definition extend_f_S {n1 n2} (p : 'I_{n1,n2}) : 'I_{n1.+1,n2.+1} :=
   fun i => match (ord_eq_dec i ord_max) with
@@ -2006,7 +2023,7 @@ End Rev_ord.
 
 Section Move_ord.
 
-(* Definition and properties of move_ord. *)
+(** Definition and properties of move_ord. *)
 
 Definition move_ord {n} (i0 i1 i : 'I_n.+1) : 'I_n.+1 :=
   match (ord_eq_dec i i1) with
@@ -2075,7 +2092,7 @@ End Move_ord.
 
 Section Transp_ord.
 
-(* Definition and properties of transp_ord. *)
+(** Definition and properties of transp_ord. *)
 
 Definition transp_ord {n} (i0 i1 i : 'I_n) : 'I_n :=
   if ord_eq_dec i i0 then i1 else if ord_eq_dec i i1 then i0 else i.
@@ -2562,6 +2579,14 @@ move=> /(cast_ord_n0_equiv_gt (lenPF_n0_rev HP)) /filterP_ord_incrF.
 rewrite Hj; easy.
 Qed.
 
+Lemma filterP_ord_ind_l_in_0_equiv :
+  forall {n} {P : 'I_n.+1 -> Prop} (HP : P ord0) (j : 'I_(lenPF P)),
+    filterP_ord j = ord0 <-> cast_ord (lenPF_ind_l_in HP) j = ord0.
+Proof.
+intros; split;
+    [apply filterP_ord_ind_l_in_0_rev | apply filterP_ord_ind_l_in_0].
+Qed.
+
 (* TODO FC (05/02/2024): use incrF in the following proofs... *)
 
 Lemma filterP_ord_ind_l_in_n0 :
@@ -2571,18 +2596,21 @@ Lemma filterP_ord_ind_l_in_n0 :
 Proof.
 (*
 intros n P HP j Hj1.
-assert (Hj2 :
+(*
+assert (Hj2' :
     (filterP_ord (Ordinal (lenPF_n0_rev HP)) < filterP_ord j)%coq_nat)
   by (apply filterP_ord_incrF; rewrite -(cast_ord_n0_equiv_gt ); apply Hj1).
-rewrite filterP_ord_ind_l_in_0 in Hj2; [| apply ord_inj; easy].
+rewrite filterP_ord_ind_l_in_0 in Hj2'; [| apply ord_inj; easy].
+*)
+assert (Hj2 : filterP_ord j <> ord0)
+  by (move: Hj1; rewrite -contra_equiv; apply filterP_ord_ind_l_in_0_rev).
+apply (lower_S_inj Hj2 (lift_S_not_first _)); rewrite lower_lift_S.
 *)
 
 intros n P HP j Hj; destruct n as [| n].
 (* *)
-exfalso; destruct (le_1_dec (lenPF_le P)) as [HP' | HP'].
-clear Hj; destruct j as [j Hj]; rewrite HP' in Hj; easy.
-contradict Hj; destruct j as [j Hj]; apply ord_inj; simpl.
-rewrite HP' in Hj; apply lt_1; apply /ltP; easy.
+exfalso; move: Hj => /ord_neq_compat; destruct j as [j Hj]; simpl.
+move: Hj => /ltP; rewrite (lenPF1_in HP); move=> /lt_1; easy.
 (* *)
 unfold filterP_ord; rewrite !(enum_val_nth ord0).
 unfold enum_val, enum_mem, mem; simpl; rewrite -!enumT enum_ordSl; simpl.
@@ -2644,6 +2672,14 @@ move=> /filterP_ord_incrF; rewrite Hj filterP_ord_ind_r_in_max;
     [apply ord_lt_irrefl | apply ord_inj; easy].
 Qed.
 
+Lemma filterP_ord_ind_r_in_max_equiv :
+  forall {n} {P : 'I_n.+1 -> Prop} (HP : P ord_max) (j : 'I_(lenPF P)),
+    filterP_ord j = ord_max <-> cast_ord (lenPF_ind_r_in_S HP) j = ord_max.
+Proof.
+intros; split;
+    [apply filterP_ord_ind_r_in_max_rev | apply filterP_ord_ind_r_in_max].
+Qed.
+
 Lemma filterP_ord_ind_r_in_nmax :
   forall {n} {P : 'I_n.+1 -> Prop} (HP : P ord_max)
       (j : 'I_(lenPF P)) (Hj : cast_ord (lenPF_ind_r_in_S HP) j <> ord_max),
@@ -2695,7 +2731,7 @@ replace (size _) with (lenPF (fun i => P (widen_S i)));
 unfold lenPF; rewrite cardE; f_equal; rewrite enumT; easy.
 Qed.
 
-(* FC (05/02/2024): this should be true...
+(* TODO FC (05/02/2024): this should be true...
 Lemma filterP_rev_ord :
   forall {n} {P : 'I_n -> Prop},
     filterP_ord \o (@rev_ord (lenPF P)) = @rev_ord n \o filterP_ord.