proposition: Lemma CK4F_remove_component (G : graph2) (C : {set G}) : C \in @components G [set~ input] -> CK4F G -> CK4F (induced2 (~: C)).
proof: Proof. move=> C_comp G_CK4F. apply: CK4F_induced2 (G_CK4F). case: G_CK4F => G_conn _. have Hi : (@input _ _ G)\notin[set~ input] by rewrite !inE negbK. apply: (@remove_component G) Hi C_comp G_conn _. rewrite setCK. exact: connected1. 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)