proposition: Lemma connected_center (G:sgraph) x (S : {set G}) : {in S, forall y, connect (restrict S (--)) x y} -> x \in S -> connected S.
proof: Proof. move => H inS y z Hy Hz. apply: connect_trans (H _ Hz). rewrite connect_symI; by [apply: H | apply: symmetric_restrict_sedge]. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)