proposition: Lemma sep_inL x V1 V2 : separation V1 V2 -> x \notin V2 -> x \in V1.
proof: Proof. move => sepV. by case/setUP : (sepV.1 x) => ->. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)