proposition: Lemma CK4F_igraph (G : graph2) (x y : G) : x \in cp G input output -> y \in cp G input output -> CK4F G -> x != y -> CK4F (igraph x y).
proof: Proof. move => Hx Hy [conn_G K4F_G] xy. split; first exact: connected_igraph. apply: subgraph_K4_free (sskeleton_add _ _) _. exact: igraph_K4F K4F_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)