proposition: Lemma diso_separation2_glue (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) : separation V1 V2 -> V1 :&: V2 = [set x;y] -> diso (glue2 (induced V1) (Sub x xV1) (Sub y yV1) (induced V2) (Sub x xV2) (Sub y yV2)) G.
proof: Proof. set x' := Sub x xV2; set y' := Sub y yV2. move => sepV capV; set H := glue2 _ _ _ _ _ _. pose g (u : H) : G := match u with inl u => val u | inr u => val (val u) end. have h_dec (u : G) : (u \in V1) + ({ uV2 : u \in V2 | Sub u uV2 \notin [set x';y'] }). { case: (boolP (u \in V1)) => [|uV1]; [by left|right]. by exists (sep_inR sepV uV1); rewrite in_set2 -!val_eqE /= -in_set2 -capV inE (negbTE uV1). } have h_dec_l u (uV1 : u \in V1) : h_dec u = inl uV1. { case: (h_dec u) => [uV1'|[uV2 p]]; first by congr(inl _); exact: bool_irrelevance. case: notF. by rewrite in_set2 -!val_eqE /= -in_set2 -capV !inE uV1 uV2 in p. } have h_dec_r u (uV2 : u \in V2) (p : Sub u uV2 \notin [set x';y']) : h_dec u = inr (Sub uV2 p). { case: (h_dec u) => [uV1|[uV2' p']]; last by congr (inr _); apply: val_inj; apply: bool_irrelevance. case: notF. by rewrite in_set2 -!val_eqE /= -in_set2 -capV !inE uV1 uV2 in p. } pose h (u : G) : H := match h_dec u with | inl uV1 => inl (Sub u uV1) | inr (exist uV2 p) => inr (Sub (Sub u uV2) p) end. have can_g : cancel g h. { move => [[u uV1]|[[u uV2] p]]; rewrite /h/g/=. + by rewrite h_dec_l. + by rewrite h_dec_r. } have can_h : cancel h g. { by move => u; rewrite /h; case: (h_dec _) => [uV1|[uV1 p]]. } have hom_g : is_dhom g. { move=> u v. rewrite [u -- v]/edge_rel/=. move: u v => [u|u] [v|v] //=. by case/orP => [/andP[/eqP->]|/andP[/eqP->]]. case/orP => [/andP[/eqP->]|/andP[/eqP->]] //; by rewrite sgP. } have hom_h : is_dhom h. { move => u v uv. rewrite /h/edge_rel/=. case: (h_dec u) => [uV1|[uV2 p]]; case: (h_dec v) => [vV1|[vV2 q]] /=. 1,4 : by rewrite induced_edge. - rewrite !inE -!val_eqE /= -in_set2 in q. rewrite -!val_eqE !induced_edge /=. have := separation_capN sepV uV1 vV2 uv; rewrite capV (negbTE q) orbF. by case/set2P => ?; subst u; rewrite eqxx uv. - rewrite !inE -!val_eqE /= -in_set2 in p. rewrite -!val_eqE !induced_edge /=; rewrite sgP in uv. have := separation_capN sepV vV1 uV2 uv; rewrite capV (negbTE p) orbF. by case/set2P => ?; subst v; rewrite eqxx uv. } exact: Diso'' hom_g hom_h. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)