proposition: Lemma CK4F_lens (G : graph2) C : CK4F G -> lens G -> C \in components (@sinterval (skeleton G) input output) -> CK4F (component C).
proof: Proof. set sI := sinterval _ _. move=> [G_conn G_K4F] G_lens C_comp. split; last by apply: subgraph_K4_free G_K4F; exact: sskeleton_subgraph_for. apply: connected_induced. exact: connected_component_set. 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)