proposition: Lemma connected_one_component (G : sgraph) (U C : {set G}) : C \in components U -> U \subset C -> connected U.
proof: Proof. move => comp_C sub_UC. have ? : connected C by apply: connected_in_components comp_C. suff : U == C by move/eqP->. by rewrite eqEsubset sub_UC components_subset. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)