proposition: Lemma split_io_edge_aux (G : graph2) (e : edge G) : e \in edges input output -> point (remove_edges [set e] ∔ [input, elabel e, output]) input output ≃2 G.
proof: Proof. rewrite inE => /andP [/eqP Es /eqP Et]. rewrite -{1}Es -{1}Et. apply: iso2_comp. apply: iso_iso2. apply: remove_edge_add. by case: G e {Es Et}. 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)