proposition: Lemma igraph_K4F_add_node (G : sgraph) (U : {set G}) : connected [set: G] -> forall x y, x \in CP U -> y \in CP U -> x != y -> K4_free (add_node G U) -> K4_free (add_edge (igraph G x y) istart iend).
proof: Proof. set H := add_node G U => G_conn x y x_cp y_cp xy H_K4F. set I := add_edge _ _ _. case: (CP_base x_cp y_cp) => [i] [o] [i_U o_U]. rewrite subUset !sub1set =>/andP[x_cpio y_cpio]. suff : K4_free (add_edge G i o) by exact: igraph_K4F => //. set K := add_edge G i o. apply: minor_K4_free H_K4F. apply: strict_is_minor. set phi : H -> K := odflt i. have preim_phi u : phi @^-1 u = Some u |: if u == i then [set None] else set0. { by apply/setP=> v; case: ifP => u_i; rewrite -mem_preim !inE ?orbF; case: v => [v|] //=; rewrite eq_sym. } have preim_phixx u : Some u \in phi @^-1 u by rewrite -mem_preim. exists phi; split. + by move=> /= u; exists (Some u). + move=> /= u; rewrite preim_phi. case: ifP => [/eqP{u}->|_]; first exact: connected2. by rewrite setU0; exact: connected1. + move=> u v /orP[]; first by [ exists (Some u); exists (Some v); split ]. move=> /orP[]/andP[_]/andP[/eqP->/eqP->]; [ exists None; exists (Some o) | exists (Some o); exists None ]; by split; rewrite // -mem_preim. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph minor) GraphTheory(checkpoint connectivity excluded set_tac)