proposition: Lemma add_edge_rmap_separation_minor (M : sgraph) (phi : M -> {set G'}) : minor_rmap phi -> (forall u, phi u \subset V1) -> minor G M.
proof: Proof. move => rmap_phi sub_phi. have [/existsP[i] y_phi_i|/existsPn Y] := boolP [exists i, y \in phi i]; last first. by have := unused_rmap_add_edge_r Y rmap_phi; apply: minor_of_rmap. have x_S : x \in S by rewrite defS !inE eqxx. have [_ [z [_ zNV1 _ xz]]] := svseparator_neighbours psepV ssepS x_S. have [p irp dis] : exists2 p : Path z y, irred p & [disjoint p & [set x]]. { apply: (@avoid_nonseperator G [set x] z y). - by apply: below_smallest ssepS _; rewrite defS cards1 cards2 xDy. - by rewrite inE eq_sym ?(sg_edgeNeq xz). - by rewrite inE eq_sym. } rewrite disjoint_sym disjoints1 in dis. have pV2: p \subset V2. { apply: contraTT isT => /subsetPn [z' z'p z'NV2]. case/psplitP: _ / z'p irp dis => {p} [p1 p2] /irred_catE [_ _ Ip] s1p. move/proper_separation_symmetry : (psepV) => psepV'. case: (separation_separates psepV'.1 zNV1 z'NV2) => _ _ /(_ p1) [s S1]. rewrite setIC -/S defS => /set2P [?|?]; subst s; first by set_tac. rewrite -(Ip y) // in z'NV2. by move/setP/(_ y) : defS; rewrite /S !inE (negbTE z'NV2) eqxx orbT andbF. } pose g := phi[upd i := phi i :|: [set v in p]] : M -> {set G}. suff: minor_rmap g by apply minor_of_rmap. have [P1 P2 P3 P4] := rmap_phi. rewrite /g; split. - move=> j; have [->{j}|jDi] := eqVneq j i; rewrite updateE //. by case/set0Pn : (P1 i) => v v_pi; apply/set0Pn; exists v; rewrite inE v_pi. - move=> j; have [->{j}|jDi] := eqVneq j i; rewrite updateE //; last first. move => u v u_pj v_pj; apply: connect_mono (P2 j u v u_pj v_pj). by apply/unused_add_edge_connect_r; rewrite (disjointFl (P3 _ _ jDi)). apply: (@connected_center _ y) => [u|]; last by rewrite inE y_phi_i. case/setUP => [u_phi_i|]; last first. + rewrite !inE srestrict_sym => u_p. case/psplitP def_p : _ / u_p => [p1 p2]. by apply: (connectRI p2) => v; rewrite !inE => ->. + have [<- //|yDu] := eqVneq y u. have/connect_irredRP-/(_ yDu) [q Iq q_sub_i] := P2 _ _ _ y_phi_i u_phi_i. have [v [yv [q' [def_q _]]]] := splitL q yDu. have v_phi_i : v \in phi i by rewrite (subsetP q_sub_i) // def_q !inE. apply: (@connect_trans _ _ v); last first. * have yNq : y \notin q' by move: Iq; rewrite def_q irred_edgeL => /andP[->]. have := add_edge_avoid q'; rewrite yNq orbT /= => /(_ isT) [q'' eq_q]. apply: (connectRI q'') => w; rewrite !inE mem_path eq_q => w_q. by rewrite (subsetP q_sub_i) // def_q !inE !mem_path w_q. * move: (yv). rewrite /edge_rel/= eqxx [v == y]eq_sym (sg_edgeNeq yv). rewrite !(andbF,andbT)/= orbC => /predU1P [eq_vx|yvG]; last first. by apply: connect1 => /=; rewrite !inE v_phi_i. subst v. apply: (@connect_trans _ _ z); last first. by apply: connect1 => /=; rewrite !inE v_phi_i sgP. by rewrite srestrict_sym; apply: (connectRI p) => w; rewrite !inE => ->. - move => j k jDk; have [i_jk|] := boolP (i \in [set j; k]); last first. rewrite !inE negb_or ![i == _]eq_sym => /andP[? ?]. by rewrite !updateE // P3. wlog ?: j k jDk {i_jk} / i = j => [W|]; last subst j. case/set2P : i_jk; last rewrite disjoint_sym; apply: W => //. by rewrite eq_sym. rewrite !updateE 1?eq_sym // disjointsU // ?P3 // disjoint_subset. apply/subsetP => v; rewrite !inE => v_p; apply: contraNN dis => v_phi_k. have: v \in S by apply/setIP; rewrite (subsetP pV2) // (subsetP (sub_phi k)). rewrite defS => /set2P [<- //|vEy]. by rewrite vEy (disjointFr (P3 _ _ jDk)) in v_phi_k. - move=> j k jk; have [i_jk|] := boolP (i \in [set j; k]); last first. { rewrite !inE negb_or ![i == _]eq_sym => /andP[A B]. rewrite !updateE // neighbor_del_edge2 // ?P4 //. all: by rewrite ?(disjointFl (P3 _ _ A)) ?(disjointFl (P3 _ _ B)). } wlog ?: j k jk {i_jk} / i = j => [W|]; last subst j. case/set2P : i_jk; first exact: W. by rewrite neighborC; apply: W; rewrite // sgP. rewrite !updateE 1?eq_sym ?sg_edgeNeq //. have/neighborP[u[v [u_phi_i v_phi_k]]] := P4 _ _ jk. have dis_ij w w' : w \in phi i -> w' \in phi k -> w' == w = false. { move => A B. apply: contraTF jk => /eqP ?; subst w'. by rewrite (rmap_disjE rmap_phi A B) sgP. } rewrite /edge_rel/= (dis_ij _ _ y_phi_i v_phi_k) !andbF. rewrite (dis_ij _ _ u_phi_i v_phi_k) /= => /orP [uv|/andP[/eqP? /eqP?]]. by apply/neighborP; exists u,v; rewrite !inE u_phi_i v_phi_k uv. by subst v u; apply/neighborP; exists z,x; rewrite !inE v_phi_k sgP xz. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries set_tac digraph) GraphTheory(sgraph treewidth minor connectivity)