proposition: Lemma vseparatorP U : reflect (vseparator U) (vseparatorb U).
proof: Proof. rewrite /vseparator /vseparatorb. apply: (iffP existsP). - move => [x /existsP [y /separatesP H]]. exists x; exists y; done. - move => [x [y H]]. exists x. apply /existsP. exists y. by apply /separatesP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)