Add and prove sorted_enum_ord, sorted_filter_enum_ord.

Proof of filterP_ord_incrF_S.
WIP: sorted_ordP.

FEM/Algebra/ord_compl.v

@@ -2257,7 +2257,7 @@ Qed.
 
 (* FC (18/12/2023): useful? *)
 Lemma unfilterP_ord_correct_in :
-  forall {n} (P : 'I_n -> Prop) {i0} (HP0 : P i0) i,
+  forall {n} {P : 'I_n -> Prop} {i0} (HP0 : P i0) {i},
     P i -> exists j, i = filterP_ord j /\ unfilterP_ord HP0 i = j.
 Proof.
 intros n P i0 HP0 i Hi; exists (unfilterP_ord HP0 i); split; [| easy].
@@ -2275,36 +2275,45 @@ 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).
+Lemma sorted_ordP :
+  forall {T : Type} {leT : rel T} {l : seq T} x0 x1,
+    reflect (forall (i : 'I_(size l)) (Hi1 : i.+1 < size l),
+        leT (nth x0 l i) (nth x1 l (Ordinal Hi1))) (sorted leT l).
 Proof.
-intros n P j Hj1.
+intros T leT l x0 x1.
+(* Use sortedP. *)
+Admitted.
 
+Lemma sorted_enum_ord : forall {n}, sorted ord_ltn (enum 'I_n).
+Proof.
+intros n; destruct n as [|n]; [rewrite (size0nil (size_enum_ord _)); easy |].
+apply /(sortedP ord0); intros i Hi1; rewrite size_enum_ord in Hi1.
+unfold ord_ltn; rewrite !nth_enum_ord//; apply ltn_trans with i.+1; easy.
+Qed.
 
-(*
-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 sorted_filter_enum_ord :
+  forall {n} (P : 'I_n -> Prop),
+    sorted ord_ltn (filter (fun i => asbool (P i)) (enum 'I_n)).
+Proof.
+intros; apply sorted_filter; [apply ord_ltn_trans | apply sorted_enum_ord].
+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.
+apply /ltP; fold (ord_ltn (filterP_ord j) (filterP_ord (Ordinal Hj1))).
+unfold filterP_ord, enum_val, enum_mem; rewrite -enumT; simpl.
+move: (sorted_filter_enum_ord P) => /sorted_ordP H0.
+assert (H1 : lenPF P = size (filter (fun i => asbool (P i)) (enum 'I_n))).
+  unfold lenPF; rewrite cardE; unfold enum_mem; do 2 f_equal.
+  rewrite filter_predT; easy.
+pose (jj := cast_ord H1 j).
+assert (Hjj1 : jj.+1 < size (filter (fun i => asbool (P i)) (enum 'I_n)))
+    by now unfold jj; simpl; rewrite -H1.
+apply (H0 (enum_default j) (enum_default (Ordinal Hj1)) jj Hjj1).
+Qed.
 
 Lemma filterP_ord_incrF :
   forall {n} (P : 'I_n -> Prop), incrF (fun j : 'I_(lenPF P) => filterP_ord j).