proposition: Lemma split_io_edge (G : graph2) (e : edge G) : e \in edges input output -> G ≃2 edge_graph2 1%CM (elabel e) 1%CM ∥ point (remove_edges [set e]) input output.
proof: Proof. move => e_io. symmetry. rewrite /par/=/g2_par/=. apply: iso2_comp. apply: merge_iso2. apply: union_add_edge_l. rewrite /=. apply: iso2_comp. apply: iso_iso2. apply: merge_add_edge. rewrite !merge_add_edgeE. apply: iso2_comp. apply: iso_iso2. apply: add_edge_iso. apply: merge_iso. apply: union_C. rewrite !merge_isoE /=. pose k (x : @two_graph _ (flat sym) tt tt) : remove_edges [set e] := match x with inl tt => input | inr tt => output end. eapply iso2_comp. apply: iso_iso2. apply: add_edge_iso. apply (merge_union_K (k := k)). - done. - abstract (case => [[]|[]] /=; apply/eqquotP; eqv). - abstract (repeat case). - rewrite /= !merge_union_KE /= {}/k. apply: iso2_comp. apply: iso_iso2. apply: iso_sym. apply: merge_add_edge. Unshelve. rewrite !(@merge_add_edgeE _ _ _ _ input (elabel e) output _). apply: iso2_comp. apply: @merge_nothing. + abstract (repeat constructor). + exact: split_io_edge_aux. 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)