proposition: Lemma same_component (G : sgraph) (x y : G) : x \in component_of y -> component_of x = component_of y.
proof: Proof. move => xy. exact: same_pblock. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)