proposition: Lemma edge_component (G : graph) (e : edge G) : @component_of G (source e) = @component_of G (target e).
proof: Proof. case: (altP (source e =P target e)) => [->//|sDt]. apply: same_pblock => //. apply/components_pblockP. have st : (source e : skeleton G) -- (target e) . { by rewrite /edge_rel/=/sk_rel sDt adjacent_edge. } by exists (prev (edgep st)). 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)