proposition: Fact separates0P x y : reflect (separates x y set0) (~~ connect edge_rel x y).
proof: Proof. apply:(iffP idP) => [nconn_xy|]. - rewrite /separates !inE. split => // p. by rewrite Path_connect in nconn_xy. - case => _ _ H. apply/negP. case/connect_irredP => p _. case: (H p) => z. by rewrite inE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)