proposition: Lemma CK4F_lens_rest (G : graph2) C : CK4F G -> lens G -> edge_set G IO == set0 -> C \in @components G (@sinterval G input output) -> CK4F (induced2 (~: C)).
proof: Proof. set sI := sinterval _ _. case/and3P: (partition_components sI). set P := components _. move=> /eqP compU /trivIsetP compI comp0 G_CK4F G_lens Eio0 C_comp. apply: CK4F_induced2 (G_CK4F). have [G_conn _] := G_CK4F. have : C \subset cover P := bigcup_sup _ C_comp. rewrite compU /sI lens_sinterval // subsetC subUset !sub1set => /andP[Gi Go]. apply: connected_center (Gi) => x Hx. have [D [D_comp DNC x_ioD]] : exists D, [/\ D \in P, D != C & x \in input |: (output |: D)]. { case: (lens_components G_CK4F G_lens Eio0 C_comp) => D D_comp DNC. case: (altP (x =P input)) => [->|Di]; last case: (altP (x =P output)) => [->|Do]. - exists D; split => //. exact: setU11. - exists D; split => //. exact: (setU1r _ (setU11 _ _)). - have x_cover : x \in cover P by rewrite compU /sI lens_sinterval // !inE negb_or Di Do. exists (pblock P x). split; first exact: pblock_mem. + rewrite inE in Hx. apply: contraNneq Hx => <-. by rewrite mem_pblock. + by rewrite !in_setU mem_pblock x_cover. } have : connect (restrict (input |: (output |: D)) (@sedge G)) input x. { apply: connected_component_set => //. exact: setU11. } apply connect_mono. apply: restrict_mono => z /=. rewrite !in_setU1. case/or3P=> [/eqP->//|/eqP->//|Hz]. by rewrite inE (disjointFr (compI D C D_comp C_comp DNC) Hz). 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)