proposition: Lemma igraph_K4F (G : sgraph) (i o x y : G) : connected [set: G] -> x \in cp i o -> y \in cp i o -> x != y -> K4_free (add_edge G i o) -> K4_free (add_edge (igraph G x y) istart iend).
proof: Proof. set H := add_edge G i o. set I := add_edge _ _ _. move=> G_conn x_cpio y_cpio xNy; apply: minor_K4_free. have iNo : i != o. { apply: contra_neq xNy => x_y. move: x_cpio y_cpio. by rewrite -{}x_y cpxx !inE =>/eqP->/eqP->. } have conn_io : connect sedge i o := connectedTE G_conn i o. wlog x_le_y : x y @I x_cpio y_cpio xNy / cpo conn_io x y. { move=> Hyp. case/orP: (cpo_total conn_io x y); first exact: Hyp. move=> ?; suff : minor (add_edge (igraph G y x) istart iend) I. { by apply: minor_trans; apply: Hyp; rewrite // 1?sg_sym 1?eq_sym. } apply: strict_is_minor; apply: iso_strict_minor. setoid_rewrite add_edge_sym. by apply: add_edge_induced_iso; first exact: interval_sym. } pose U2 := [set x; y]. have [i_Px o_Py] : i \in bag U2 x /\ o \in bag U2 y. { split; apply/bagP=> z; rewrite CP_set2 (cpo_cp x_cpio y_cpio x_le_y); move=> /andP[z_cpio] /andP[x_le_z z_le_y]. + rewrite (cpo_cp (mem_cpl i o) z_cpio); repeat (apply/andP; split) => //; exact: cpo_min. + have o_cpio : o \in cp i o by rewrite cp_sym mem_cpl. rewrite cp_sym (cpo_cp z_cpio o_cpio); repeat (apply/andP; split) => //; exact: cpo_max. } case: (collapse_bags G_conn U2 x _); first by rewrite !inE eqxx. set T := U2 :|: _. have {T}-> : T = interval x y. { rewrite {}/T {-3}/U2 /interval bigcup_setU !bigcup_set1. congr ([set x; y] :|: _). rewrite -setTD (sinterval_bag_cover G_conn xNy). rewrite setUAC setDUl setDv set0U; apply/setDidPl. rewrite disjoint_sym disjoints_subset subUset -!disjoints_subset. by rewrite {2}sinterval_sym !interval_bag_disj //; apply: CP_extensive; rewrite !inE eqxx. } rewrite -[induced _]/(igraph G x y). set Gxy := igraph G x y in I *. move=> phi [[phi_surj preim_phi_conn phi_edge] preim_phi preim_phixy]. apply: strict_is_minor. exists phi; split; first exact: phi_surj. + move=> u; have u_I : val u \in interval x y := valP u. case: (boolP (val u \in U2)) => u_xy. - rewrite preim_phixy //. apply: add_edge_connected. apply: (@connected_bag G G_conn (val u) U2). exact: CP_extensive. - rewrite preim_phi; first exact: connected1. by rewrite inE u_xy u_I. + move=> u v /orP[]. - move/phi_edge => [u'] [v'] [? ? uv']. by exists u'; exists v'; split; rewrite /edge_rel //= uv'. - wlog [-> -> _] : u v / u = istart /\ v = iend. { case/(_ istart iend); [ by split | by rewrite /= !eqxx xNy | ]. move=> u' [v'] [? ? ?]. have ? : v' -- u' by rewrite sg_sym. case/orP=> /andP[_]/andP[/eqP->/eqP->]; [ by exists u'; exists v' | by exists v'; exists u' ]. } rewrite 2?preim_phixy ?inE ?eqxx // ![val _]/=. by exists i; exists o; split; rewrite /edge_rel //= iNo !eqxx. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph minor) GraphTheory(checkpoint connectivity excluded set_tac)