proposition: Lemma lens_components (G : graph2) C : CK4F G -> lens G -> edge_set G IO == set0 -> C \in components (@sinterval G input output) -> exists2 D, D \in components (@sinterval G input output) & D != C.
proof: Proof. set sI := sinterval _ _. case/and3P: (partition_components sI). set P := components _. move=> /eqP compU compI comp0 [G_conn G_K4F] G_lens Eio0 C_comp. have iNo : input != output :> G by case/and3P: G_lens => _ _ /(@sg_edgeNeq (link_graph G))->. have Nio : ~~ @adjacent _ _ G input output. { apply: contraTN Eio0 => io. apply/set0Pn. case/existsP: io => e. rewrite inE => He. exists e. by case/orP: He; apply: edge_in_set; rewrite in_set2 eqxx. } have : 1 < #|P| by exact: split_K4_nontrivial. rewrite (cardD1 C) C_comp add1n ltnS => /card_gt0P[/= D]. rewrite !inE => /andP[DNC] D_comp. by exists D. 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)