proposition: Lemma separation_separates x y V1 V2: separation V1 V2 -> x \notin V2 -> y \notin V1 -> separates x y (V1 :&: V2).
proof: Proof. move => sepV Hx Hy. split; rewrite ?inE ?negb_and ?Hx ?Hy // => p. case: (@split_at_first G (mem V2) x y p y) => // ; rewrite ?(sep_inR sepV) //. move => z [p1 [p2 [H1 H2 H3]]]. rewrite inE in H2. exists z; rewrite ?H1 !inE ?H2 // andbT. case: (@splitR G x z p1) => [|z0 [p1' [z0z H4]]]. { by apply: contraTneq H2 => <-. } apply: contraTT (z0z) => Hz1. rewrite sepV ?inE //. apply: contraTN (z0z) => H0. by rewrite [z0]H3 ?sgP // H4 !inE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)