proposition: Lemma svseparator_uniq x y S: smallest vseparator S -> separates x y S -> S != set0 -> exists2 p : Path x y, irred p & exists! z, z \in p /\ z \in S.
proof: Proof. Abort. Lemma separation_connected_same_component V1 V2: separation V1 V2 -> forall x0 x, x0 \notin V2 -> connect (restrict [predC (V1:&:V2)] sedge) x0 x -> x \notin V2. Proof. set S := V1 :&: V2. move => sepV x0 x x0NV2. case: (boolP (x0==x)) => [/eqP ? | x0x]; first by subst x0. case/(connect_irredRP x0x) => p _ /subsetP Hp. case: (boolP(x \in V2)) => // xV2. case: (@split_at_first G (mem V2) x0 x p x) => //. move => z [p1 [p2 [H1 H2 H3]]]. rewrite inE /= in H2. case: (altP (x0 =P z)) => ?; first by subst x0; contrab. case: (@splitR G x0 z p1) => [|z0 [p1' [z0z H4]]] //. apply: contraTT (z0z) => _. rewrite sepV //. + apply: contraTN (z0z) => z0V2. by rewrite [z0]H3 ?sgP // H4 !inE. + have ? : (z \notin S) by apply: Hp; rewrite H1 !inE. by subst S; set_tac. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)