proposition: Lemma comp_exit (G : graph2) (C : {set G}) : connected [set: skeleton G] -> input == output :> G -> C \in @components G [set~ input] -> exists2 z : skeleton G, z \in C & z -- input.
proof: Proof. move=> G_conn Eio C_comp. case/and3P: (@partition_components G [set~ input]) => /eqP compU compI comp0. have /card_gt0P[a a_C] : 0 < #|C|. { rewrite card_gt0. by apply: contraTneq C_comp =>->. } have aNi : a \in [set~ input]. { rewrite -compU. by apply/bigcupP; exists C. } rewrite -{C C_comp a_C}(def_pblock compI C_comp a_C). case/connect_irredP: (connectedTE G_conn a input) => p. move: (aNi); rewrite !inE. case/(splitR p) => [z][q][zi] {p}->. rewrite irred_cat. case/and3P=> _ _ /eqP/setP/(_ input). rewrite !inE eq_sym sg_edgeNeq // andbT => /negbT iNq. exists z => //. rewrite pblock_equivalence_partition // ?inE ?(sg_edgeNeq zi) //. + apply: (connectRI q) => x. rewrite !inE. by apply: contraTneq =>->. + exact: sedge_equiv_in. Qed.
imports: Coq(RelationClasses Morphisms Setoid) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(bij set_tac digraph sgraph minor checkpoint) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(skeleton bounded equiv extraction_def)