diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index 7e2aeb94eb3018576bd47467d993cd215f832011..5e210042366d06c0a1307c58ebe5178a8691a192 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -2576,14 +2576,4 @@ replace (size _) with (lenPF (fun i => P (widen_S i)));
 unfold lenPF; rewrite cardE; f_equal; rewrite enumT; easy.
 Qed.
 
-(* FC (19/12/2023): check this statement!
-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.