proposition: Lemma CK4F_component (G : graph2) (x : G) : K4_free (sskeleton G) -> CK4F (component1 x).
proof: Proof. move => K4F_G. split => //. - apply: connected_induced. exact: connected_component_of. - apply: subgraph_K4_free (sub_pointxx _) _. exact: induced_K4_free. Qed.
imports: Coq(RelationClasses Morphisms Setoid) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries set_tac) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(equiv setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 ptt mgraph2_tw2 skeleton) GraphTheory(bounded extraction_def extraction_iso excluded)