Proof of filterP_cast_ord_incrF.

WIP: filterP_ord_incrF_S.

FEM/Algebra/ord_compl.v

@@ -2275,14 +2275,40 @@ Lemma unfilterP_ord_inj :
       unfilterP_ord HP0 i = unfilterP_ord HP0 j -> i = j.
 Proof. move=>> Hi Hj; apply enum_rank_in_inj; apply /asboolP; easy. Qed.
 
+Lemma filterP_ord_incrF_S :
+  forall {n} (P : 'I_n -> Prop), incrF_S (fun j : 'I_(lenPF P) => filterP_ord j).
+Proof.
+intros n P j Hj1.
+
+
+(*
+destruct (lt_eq_lt_dec (filterP_ord j1) (filterP_ord j2))
+    as [[H | H] | H]; [easy | exfalso..].
+apply ord_inj, filterP_ord_inj in H; subst; contradict Hj; apply Nat.lt_irrefl.
+*)
+
+(*
+enum_val
+nth sorted
+
+mem : pT -> mem_pred T
+enum_mem : mem_pred T -> seq T := filter Finite.enum mA
+enum A := (enum_mem (mem A))
+enum_val : 'I_#|[eta A]| -> T := nth (enum_default i) (enum A) i
+enum_rank : T -> 'I_#|[eta T]| := enum_rank_in (erefl true) x
+enum_rank_in : x0 \in A -> T -> 'I_#|[eta A]|
+
+nth_image : nth y0 [seq f x | x in A] i = f (enum_val i)
+enum_val_nth : enum_val i = nth x (enum A) i
+enum_valK : cancel enum_val enum_rank
+enum_rankK : cancel enum_rank enum_val
+nth_codom : nth y0 (codom f) i = f (enum_val i)
+*)
+Admitted.
+
 Lemma filterP_ord_incrF :
   forall {n} (P : 'I_n -> Prop), incrF (fun j : 'I_(lenPF P) => filterP_ord j).
-Proof.
-intros n P j1 j2 Hj.
-
-
-
-Admitted.
+Proof. intros; apply incrF_equiv, filterP_ord_incrF_S. Qed.
 
 Lemma filterP_cast_ord_incrF :
   forall {n1 n2} {P1 : 'I_n1 -> Prop} {P2 : 'I_n2 -> Prop}