proposition: Lemma sub_filter (T : eqType) (p : {pred T}) (s : seq T) : {subset [seq x <- s | p x] <= s}.
proof: Proof. by move=> x; rewrite mem_filter => /andP[_ ->]. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)