proposition: Lemma CK4F_sub (G : graph2) (V : {set G}) x : @connected G V -> CK4F G -> CK4F (point (induced V) x x).
proof: Proof. move => conV CK4F_G. split. - exact: connected_induced. - apply: subgraph_K4_free (sub_pointxx _) _. apply: induced_K4_free. apply CK4F_G. 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)