proposition: Lemma connected_component_of (G : sgraph) (x : G) : connected (component_of x).
proof: Proof. apply: connected_in_components. exact: component_of_components. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)