proposition: Lemma separate_nonadjacent x y : x != y -> ~~ x -- y -> proper_separation [set~ x] [set~ y].
proof: Proof. move => xDy xNy. split; last by exists y; exists x; rewrite !inE !eqxx. split => [z | x1 x2]. - rewrite !inE -negb_and. by apply: contraNN xDy => /andP[/eqP->/eqP->]. - rewrite !inE !negbK sg_sym => /eqP-> /eqP->. by rewrite (negbTE xNy). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)