proposition: Lemma minimal_separation x y : x != y -> ~~ x -- y -> exists V1 V2, proper_separation V1 V2 /\ smallest vseparator (V1 :&: V2).
proof: Proof. move => xDy xNy. move/proper_vseparator/vseparatorP : (separate_nonadjacent xDy xNy) => sep. case: (arg_minnP (fun S => #|S|) sep) => U /vseparatorP sepU HU {sep xDy xNy}. move: (vseparator_separation sepU) => [V1 [V2 [ps UV]]]. exists V1; exists V2. repeat split => //; rewrite -UV // => V /vseparatorP. exact: HU. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)