Some cleaning.

filterP_rev_ord is wrong (when P is not symmetric).

FEM/Algebra/ord_compl.v

@@ -1584,7 +1584,6 @@ Section Skip_Insert_ord.
 
 (* Definitions and properties of skip_ord/insert_ord. *)
 
-(* TODO FC (02/03/2023): n -> n.-1 could be OK... *)
 Definition skip_ord {n} (i0 : 'I_n.+1) (j : 'I_n) : 'I_n.+1 :=
   lift i0 (cast_ord (pred_Sn n) j).
 
@@ -2758,24 +2757,6 @@ apply (Rg_correct (unfilterP_ord HP' (lower_S Hi1)));
     rewrite filterP_unfilterP_ord_in// lift_lower_S; easy.
 (* *)
 intros i [j _]; split; [apply lift_S_not_first | apply filterP_ord_correct].
-(* was:
-intros n P HP j Hj; destruct n as [| n].
-(* *)
-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.
-unfold in_mem; simpl; case_eq (asbool (P ord0)); intros HP'.
-2: move: HP' => /(elimF (asboolP _)) //.
-apply cast_ord_n0 in Hj; rewrite nth_cons_r//
-    filter_map (nth_map ord0); unfold lift_S; f_equal.
-destruct j as [j Hj1]; simpl in *.
-rewrite ltn_subLR; try now apply /ltP; apply Nat.neq_0_lt_0.
-replace (size _) with (lenPF (fun i => P (lift ord0 i)));
-    try now rewrite -lenPF_ind_l_in.
-unfold lenPF; rewrite cardE; f_equal; rewrite enumT; easy.
-*)
 Qed.
 
 (* TODO FC (05/02/2024): use incrF in the following proofs... *)
@@ -2886,14 +2867,4 @@ replace (size _) with (lenPF (fun i => P (widen_S i)));
 unfold lenPF; rewrite cardE; f_equal; rewrite enumT; easy.
 Qed.
 
-(* 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.
-Proof.
-intros n P; apply fun_ext; intros j.
-rewrite !comp_correct. unfold filterP_ord.
-apply ord_inj. simpl.
-Aglopted.*)
-
 End FilterP_ord.