proposition: Lemma separatorI A B S : (forall (a b : G) (p : Path a b), irred p -> a \in A -> b \in B -> exists2 s, s \in S & s \in p) -> separator A B S.
proof: Proof. move => H a b p aA bB. case: (uncycle p) => p' sub_p Ip. case: (H _ _ p') => //. move => s sS /sub_p sp. by exists s. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)