diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index 38959363ac982e4ad551dc056581e0f62eebea9b..d3a0e8552006e9e2a78604eee9f919c700ae0941 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -2527,6 +2527,14 @@ Lemma filterP_ord_ind_l_in_n0 :
       (j : 'I_(lenPF P)) (Hj : cast_ord (lenPF_ind_l_in HP) j <> ord0),
     filterP_ord j = lift_S (filterP_ord (lower_S Hj)).
 Proof.
+(*
+intros n P HP j Hj1.
+assert (Hj2 :
+    (filterP_ord (Ordinal (lenPF_n0_rev HP)) < filterP_ord j)%coq_nat).
+  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].
+*)
+
 intros n P HP j Hj; destruct n as [| n].
 (* *)
 exfalso; destruct (le_1_dec (lenPF_le P)) as [HP' | HP'].