proposition: Lemma split_component (G : graph2) (C : {set G}) : edge_set G IO == set0 -> C \in @components G (~: IO) -> G ≃2 component C ∥ induced2 (~: C).
proof: Proof. move=> NEio C_comp. case/and3P: (@partition_components G (~: IO)) => /eqP compU compI comp0n. have : C \subset ~: IO by rewrite -compU; apply/subsetP => x; exact: mem_cover. rewrite subsetC subUset !sub1set => /andP[iNC oNC]. rewrite induced2_induced. apply: iso_split_par2. - rewrite setUA setIUl setICr setU0. exact: subsetIl. - by rewrite -!setUA setUCr !setUT. - rewrite -(eqP NEio). apply/setP=> e; rewrite !inE. rewrite andbACA !orbA andb_orl andbN orbF. rewrite [_ && (target e \notin C)]andb_orl andbN orbF andbACA. apply/idP/idP => [/andP[->]//|He]. rewrite He /=. rewrite !inE in iNC oNC. case/andP: He => /orP[]/eqP-> /orP[]/eqP->; by rewrite ?iNC ?oNC. - apply/eqP. rewrite eqEsubset subsetT /=. apply/subsetP=> e _. rewrite !inE. case: (altP (source e =P target e)) => [<-|He]. by rewrite !andbb -!orbA orbN. rewrite -negb_or orbC -implybE. apply/implyP. have {He} : @sedge G (source e) (target e) by rewrite /=/sk_rel He adjacent_edge. move: {e} (source e) (target e). suff Hyp (x y : G) : @sedge G x y -> x \in C -> [|| y == input, y == output | y \in C]. { move=> x y xy /orP[]H; rewrite H !orbT /= ?andbT; first exact: Hyp xy H. move: H. have : @sedge G y x by rewrite sg_sym. exact: Hyp. } move=> xy Hx. have := component_exit xy C_comp Hx. by rewrite !inE negbK orbA. 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)