proposition: Lemma CK4F_redirect (G : graph2) C : CK4F G -> input == output :> G -> C \in @components G [set~ input] -> CK4F (redirect C).
proof: Proof. move => CK4F_G Eio HC. have D := @partition_components G [set~ input]. have Csub: C \subset [set~ input]. { rewrite -(cover_partition D). apply/subsetP => z Hz. exact: mem_cover HC _. } rewrite /redirect. case: pickP => [z /andP [Z1 Z2]|_]; last exact: CK4F_one. have conn_iC : @connected G (input |: C). { apply: (@connectedU_edge G _ _ input z) => //. - by rewrite set11. - rewrite /edge_rel/=/sk_rel Z2 andbT. move/(subsetP Csub) in Z1. by rewrite !inE eq_sym in Z1. - apply: connected1. - apply: connected_in_components HC. } split. - apply: connected_induced. by rewrite [z |: C]setU1_mem. - have: K4_free (induced (input |: C)). { apply: induced_K4_free. by apply CK4F_G. } apply: iso_K4_free. setoid_rewrite <-sskeleton_adjacent. by rewrite (setU1_mem Z1). by rewrite adjacent_induced. Qed.
imports: Coq(RelationClasses Morphisms Setoid Lia) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(digraph sgraph minor checkpoint cp_minor) GraphTheory(setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 skeleton bounded)