proposition: Lemma vseparator_separation S : vseparator S -> exists V1 V2, proper_separation V1 V2 /\ S = V1 :&: V2.
proof: Proof. move => [x [y sepS]]; have xDy := separatesNeq sepS. set U := locked [set z in ~: S | connect (restrict (~: S) sedge) x z]. set V1 := U :|: S; set V2 := ~: U; exists V1, V2. move: sepS => [S1 S2 P12]; split; first split; first split. - by rewrite /V1 /V2; set_tac. - move=> u v. rewrite !inE negbK negb_or => Hu /andP [Hv1 Hv2]. apply: contraNF Hv1 => uv. move: (Hu); rewrite /U -lock !inE Hv2 /= => /andP [uNS H]. by apply: connect_trans H (connect1 _); rewrite /= !inE uNS Hv2. - exists x,y; split; first by rewrite !inE negbK /U -lock !inE connect0. rewrite !inE negb_or S2 andbT; apply: contraTN isT. rewrite /U -lock !inE => /andP [_ /connect_irredRP -/(_ xDy) [p Ip subS]]. by have [s ?] := P12 p; set_tac. - apply/setP => z;rewrite !inE andb_orl andbN /= andb_idr // => z_S. by rewrite /U -lock !inE z_S. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)