proposition: Lemma avoid_nonseperator U x y : ~ vseparator U -> x \notin U -> y \notin U -> exists2 p : Path x y, irred p & [disjoint p & U].
proof: Proof. move => nsep_u xU yU. case: (altP (x =P y)) => [?|A];first subst y. - exists (idp x); first exact: irred_idp. rewrite (@eq_disjoint1 _ x) // => y. by rewrite mem_idp. - have/separatesNE/connect_irredRP : ~ separates x y U by apply vseparatorNE. case => // p irr_p. rewrite -disjoint_subset. by exists p. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)