proposition: Lemma component_exit (G : sgraph) (V C : {set G}) (x y : G) : x -- y -> C \in components V -> x \in C -> y \in ~: V :|: C.
proof: Proof. move=> xy C_comp x_C. rewrite !inE -implybE. apply/implyP => y_V. case/and3P: (partition_components V) => /eqP compU compI comp0n. have x_V : x \in V by rewrite -compU; apply/bigcupP; exists C. rewrite -(def_pblock compI C_comp x_C) pblock_equivalence_partition //; last exact: sedge_equiv_in. apply: (connectRI (edgep xy)) => z; rewrite mem_edgep. by case/orP=> /eqP->. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)