proposition: Lemma connectedU_common_point (G : sgraph) (U V : {set G}) (x : G): x \in U -> x \in V -> connected U -> connected V -> connected (U :|: V).
proof: Proof. move => xU xV conU conV. apply connected_center with x; last by rewrite !inE xU. move => y. case/setUP => [yU|yV]. - apply: connect_restrict_mono (conU _ _ xU yU); exact: subsetUl. - apply: connect_restrict_mono (conV _ _ xV yV); exact: subsetUr. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)