proposition: Lemma separatorPn (A B S : {set G}) : reflect (exists x y (p: IPath x y), [/\ x \in A, y \in B & [disjoint p & S]]) (~~ separatorb A B S).
proof: Proof. rewrite negb_forall_in. apply: (iffP exists_inP). - case => x xA /forall_inPn [y] yB /forallPn [p] /exists_inPn H. exists x; exists y; exists p; split => //. apply/disjointP => z Z1 /H. by rewrite Z1. - case => x [y] [p] [aA yB /disjointP D]. exists x => //. apply/forall_inPn; exists y => //. apply/forallPn; exists p. apply/exists_inPn => z /D H. exact/negP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)