proposition: Lemma nth_filterP' A (f : A -> Prop) (l : list A) n d (LT : n < length l) (F: f (nth n l d)): nth (length (filterP f (map (fun i => nth i l d) (List.seq 0 n)))) (filterP f l) d = nth n l d.
proof: Proof. revert n F LT; induction l using rev_induction; ins; desf; ins; try lia. rewrite filterP_app, length_app in *. destruct (lt_dec n (length l)). { rewrite !app_nth1 in *; ins. specialize_full IHl; eauto; desf. rewrite <- IHl. do 3 f_equal; apply map_ext_in; ins; rewrite in_seq0_iff in *; rewrite app_nth1; ins; lia. erewrite <- map_nth_seq with (a := 0) (l := l) (f := fun i => nth i (l ++ a :: nil) d) at 1; auto using app_nth1. rewrite (seq_split0 l0), map_app, filterP_app, length_app; ins; desf; ins; try lia. } ins; desf; ins. all: assert (n = length l) by lia; desf. all: rewrite app_nth2, Nat.sub_diag in F; ins; desf; try lia. rewrite map_nth_seq with (d := d). rewrite !app_nth2, ?Nat.sub_diag; ins. ins; rewrite app_nth1; ins. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation