proposition: Lemma diso_separation2 (G : sgraph) (V1 V2 : {set G}) (x y : G) (xV1 : x \in V1) (xV2 : x \in V2) (yV1 : y \in V1) (yV2 : y \in V2) (G1 := induced V1) (G2 := induced V2) (G12 := (G1 ∔ G2)%sg) (x1 : G12 := inl (Sub x xV1)) (x2 : G12 := inr (Sub x xV2)) (y1 : G12 := inl (Sub y yV1)) (y2 : G12 := inr (Sub y yV2)) (y1Gm : y1 != x2) (y2Gm : y2 != x2) : separation V1 V2 -> V1 :&: V2 = [set x; y] -> x -- y -> diso (smerge2 (smerge2 (G1 ∔ G2) x1 x2) (Sub y1 y1Gm) (Sub y2 y2Gm)) G.
proof: Proof. move=> sepV capV xy. have := diso_separation2_glue xV1 xV2 yV1 yV2 sepV capV. apply: diso_comp. apply: smerge2_glue2 => //. by rewrite -val_eqE /= sg_edgeNeq. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)