proposition: Lemma component_exchange (G : sgraph) (x y : G) : (y \in component_of x) = (x \in component_of y).
proof: Proof. apply/components_pblockP/components_pblockP. all: case => p _; by exists (prev p). Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)