proposition: Lemma diso_separation V1 V2 : separation V1 V2 -> [disjoint V1 & V2] -> diso ((induced V1) ∔ (induced V2))%sg G.
proof: Proof. move => sepV disV; have V2E : V2 = ~: V1. { apply/setP => x; rewrite inE; apply/idP/idP => Hx. by rewrite (disjointFl disV Hx). exact: sep_inR Hx. } rewrite V2E; apply: ssplit_disconnected => x y ? ?. by rewrite sepV // V2E inE negbK. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)