proposition: Lemma separatesI x y (U : {set G}) : [/\ x \notin U, y \notin U & forall p : Path x y, irred p -> exists2 z, z \in p & z \in U] -> separates x y U.
proof: Proof. case => S1 S2 S3. split => // p. case: (uncycle p) => p' sub_p Ip'. case: (S3 _ Ip') => z Z1 Z2. exists z => //. exact: sub_p. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)