proposition: Lemma connected_card_gt1 (G : sgraph) (S : {set G}) : connected S -> {in S &, forall x y, x != y -> exists2 z, z \in S & x -- z }.
proof: Proof. move=> conn_S x y x_S y_S xNy. move: conn_S => /(_ x y x_S y_S)/(connect_irredRP xNy)[p] _ /subsetP p_S. case: (splitL p xNy) => [z] [xz] [p'] [_ eqi_p']. exists z; last by []; apply: p_S. by rewrite in_collective nodesE inE -eqi_p' path_begin. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)