proposition: Lemma svseparator_neighbours V1 V2 s : proper_separation V1 V2 -> smallest vseparator (V1 :&: V2) -> s \in V1 :&: V2 -> exists x1 x2, [/\ x1 \notin V2, x2 \notin V1, s -- x1 & s -- x2].
proof: Proof. wlog: V1 V2 / [forall x1, (x1 \notin V2) ==> ~~ s -- x1]. { move => H ps ss sS. case (boolP [forall x1, (x1 \notin V2) ==> ~~ s -- x1]). - move => HH. apply (H V1 V2) => //. - move => /forall_inPn [x1 x1V /negPn sx1]. case (boolP [forall x, (x \notin V1) ==> ~~ s -- x]). + move => HH. rewrite setIC in sS ss. case (H V2 V1) => //. * by apply proper_separation_symmetry. * move => y [z [? ? ? ?]]. exists z; exists y. split; done. + move => /forall_inPn [x2 x2V sx2]. exists x1; exists x2. split => //; by apply negbNE. } move => /forall_inP Hwlog [sepV [x1] [x2] [x1V12 x2V21]] smallS sS. pose S' := V1 :&: V2:\ s. suff: vseparator S'. - move => sS'. case: (below_smallest (V := S') smallS) => //. by rewrite /S' (cardsD1 s (V1 :&: V2)) sS. - exists x1; exists x2. split; try by rewrite /S' notinD. + move => p. case: (@split_at_first G (mem V2) x1 x2 p x2) => //. { by rewrite (sep_inR sepV x2V21). } move => z [p1 [p2 [H1 H2 H3]]]. rewrite inE in H2. exists z; first by rewrite H1 !inE. case: (@splitR G x1 z p1). { apply: contraTN isT => /eqP ?. subst x1; contrab. } move => z0 [p' [z0z Hp']]. have z0V1: z0 \notin V2. { apply: contraTN (z0z) => ?. by rewrite [z0]H3 ?sgP // Hp' !inE. } rewrite !inE H2 andbT. apply/andP; split. * apply: contraTN (z0z) => /eqP->. by rewrite sgP Hwlog. * apply: contraTT (z0z) => ?. by rewrite sepV. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)