proposition: Fact separatesNeq x y U : separates x y U -> x != y.
proof: Proof. case => Hx _ Hp. apply: contraNN Hx => /eqP C. subst y. case: (Hp (idp x)). move => ?. by rewrite mem_idp => /eqP->. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)