WIP: simpler proof of filterP_ord_ind_l_in_n0.

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'].