proposition: Lemma connectedU_edge (G : sgraph) (U V : {set G}) (x y : G) : x \in U -> y \in V -> x -- y -> connected U -> connected V -> connected (U :|: V).
proof: Proof. move=> x_U y_V xy U_conn V_conn u v u_UV v_UV. have subl : {subset mem U <= mem (U :|: V)} by move=> ?; rewrite !inE =>->. have subr : {subset mem V <= mem (U :|: V)} by move=> ?; rewrite !inE =>->. case: (altP (u =P v)) => [->|uNv]; first exact: connect0. wlog [u_U v_V] : u v uNv {u_UV v_UV} / u \in U /\ v \in V. { move=> Hyp. move: u_UV v_UV. rewrite !inE. move=> /orP[u_U | u_V] /orP[v_U | v_V]. - apply: connect_mono (U_conn u v u_U v_U). exact: restrict_mono. - exact: Hyp. - rewrite srestrict_sym. apply: Hyp; by [rewrite eq_sym |]. - apply: connect_mono (V_conn u v u_V v_V). exact: restrict_mono. } apply: (@connect_trans _ _ y); last first. { apply: connect_mono (V_conn y v y_V v_V). exact: restrict_mono. } apply: (@connect_trans _ _ x). { apply: connect_mono (U_conn u x u_U x_U). exact: restrict_mono. } by apply: connect1; rewrite /= !inE x_U y_V xy. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)