proposition: Lemma iso2_disconnected_component (G : graph2) x : input \in ~: @component_of G x -> output \in ~: @component_of G x -> G ≃2 top · (component1 x · top) ∥ component (~: @component_of G x).
proof: Proof. move => iC oC. symmetry. rewrite (component_induced iC oC). set C := component_of _. rewrite /component1. set G1 := point _ _ _. set G2 := point _ _ _. rewrite -> dot2A,iso2_TGT. simpl. setoid_rewrite -> par_component. rewrite /G1 /G2 /=. have comp_C : C \in @components G [set: G]. apply: component_of_components. Iso2 (iso_component comp_C). Qed.
imports: Coq(RelationClasses Morphisms Setoid) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries set_tac) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(equiv setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 ptt mgraph2_tw2 skeleton) GraphTheory(bounded extraction_def extraction_iso excluded)