proposition: Lemma induced_K4_free (G : graph2) (V : {set G}) : K4_free (sskeleton G) -> K4_free (induced V).
proof: Proof. apply: minor_K4_free. apply: (minor_trans (y := skeleton G)). apply: sub_minor. apply: skel_sub. apply: sub_minor. apply: sub_sub. exact: induced_sub. 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)