proposition: Lemma subseq_of_subset (T : finType) (A : pred T) (s : seq T) n : uniq s -> {subset A <= s} -> n <= #|A| -> exists p : seq T, [/\ {subset p <= A}, size p = n & subseq p s].
proof: Proof. move => uniq_s subAs leq_n_A; exists (take n [seq x <- s | x \in A]); split. - by move=> x /mem_take; rewrite mem_filter => /andP[->]. - rewrite size_takel // -(card_uniqP _) ?filter_uniq //. apply: leq_trans leq_n_A _; apply/subset_leq_card/subsetP => x x_A. by rewrite mem_filter x_A subAs. - apply: subseq_trans (take_subseq _ _) _. exact: filter_subseq. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)