proposition: Lemma nth_filterP A (f : A -> Prop) (l : list A) i d (LT : i < length (filterP f l)) : exists n, n < length l /\ nth i (filterP f l) d = nth n l d /\ i = length (filterP f (map (fun i => nth i l d) (List.seq 0 n))).
proof: Proof. revert i LT; induction l using rev_induction; ins; desf; ins; try lia. rewrite filterP_app, length_app in *. destruct (lt_dec i (length (filterP f l))). { specialize_full IHl; eauto; desf. exists n; rewrite !app_nth1; splits; ins; try lia. do 2 f_equal; apply map_ext_in; ins; rewrite in_seq0_iff in *; rewrite app_nth1; ins; lia. } ins; desf; ins; try lia. assert (i = length (filterP f l)) by lia; desf. exists (length l); splits; try lia. rewrite !app_nth2, !Nat.sub_diag; ins; try lia. do 2 f_equal. symmetry; eapply map_nth_seq with (d := d); ins. apply app_nth1; ins. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation