proposition: Lemma separatesP x y U : reflect (separates x y U) (separatesb x y U).
proof: Proof. apply: (iffP and3P) => [[? ? A]|[? ? A]]. - apply: separatesI. split => // p Ip. move/forallP/(_ (Build_IPath Ip)) : A. case/exists_inP => z Z1 Z2. by exists z. - split => //. apply/forallP => p. by move/exists_inP : (A p). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)