fact: Definition separator (A B S : {set G}) := forall (a b : G) (p : Path a b), a \in A -> b \in B -> exists2 s, s \in S & s \in p.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)