proposition: Lemma mem_bigcup (T1 T2 : finType) (F : T1 -> {set T2}) (P : pred T1) z y : P y -> z \in F y -> z \in \bigcup_(x | P x) F x.
proof: Proof. move => Py zF. by apply/bigcupP; exists y; rewrite ?yA. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)