proposition: Lemma vseparatorNE U x y : ~ vseparator U -> ~ separates x y U.
proof: Proof. move => nsepU sepU. by apply nsepU; exists x; exists y. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)