proposition: Lemma edge_set_component (G : graph) (C : {set skeleton G}) (e : edge G) : C \in @components G [set: G] -> (source e \in C) = (target e \in C).
proof: Proof. move => comp_C. apply/idP/idP. - move => inC. rewrite (mem_component comp_C inC). by rewrite edge_component (@in_component_of G). - move => inC. rewrite (mem_component comp_C inC). by rewrite -edge_component (@in_component_of G). 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)