proposition: Lemma edge_comp (G : graph) (C : {set G}) (e : edge G): C \in components [set: skeleton G] -> (e \in edge_set C) + (e \in edge_set (~: C))%type.
proof: Proof. move => comp_C. case: (boolP (source e \in C)) => p; [left|right]. - by rewrite inE -(edge_set_component comp_C) p. - by rewrite !inE -(edge_set_component comp_C) p. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)