proposition: Lemma separatesNE x y (U : {set G}) : x \notin U -> y \notin U -> ~ separates x y U -> connect (restrict [predC U] edge_rel) x y.
proof: Proof. move => xU yU /(introN separatesP). rewrite /separatesb xU yU !negb_and //= negb_forall. case: (altP (x =P y)) => [<-|xDy H]; first by rewrite connect0. apply/connect_irredRP => //. case/existsP : H => p Hp. exists p => //. exact/subsetP/(exists_inPn Hp). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)