proposition: Lemma proper_vseparator V1 V2 : proper_separation V1 V2 -> vseparator (V1 :&: V2).
proof: Proof. case => Hsep [x] [y] [Hx Hy]. exists x. exists y. exact: separation_separates. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)