proposition: Lemma opn_separates x y : x != y -> ~~ x -- y -> separates x y N(x).
proof: Proof. move=> xDy xNy. split; rewrite ?inE ?sg_irrefl // => p. case: (splitL p) => // x' [xx'] [p'] [->] _. by exists x'; rewrite !inE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)