proposition: Lemma split_pip (G : graph2) : connected [set: skeleton G] -> input != output :> G -> G ≃2 @bgraph _ _ G IO input · (@igraph _ _ G input output · @bgraph _ _ G IO output).
proof: Proof. move => conn_G Dio. symmetry. have [Hi Ho] : input \in @CP (skeleton G) IO /\ output \in @CP (skeleton G) IO by split; apply: CP_extensive; rewrite !inE eqxx. rewrite-> dot2A. rewrite /= {1}/bgraph /igraph /induced. setoid_rewrite merge_subgraph_dot=>//=. 2: exact: interval_bag_edges_disj. 2: move => x; exact: (@bag_interval_cap G). rewrite /bgraph/induced. setoid_rewrite-> merge_subgraph_dot => //=. move: (union_bij_proofL _ _) => Pi. move: (union_bij_proofR _ _) => Po. move: (consistentU _ _) => con1. apply iso2_subgraph_forT => //=. move => x. move: (sinterval_bag_cover conn_G Dio). have: x \in [set: G] by []. rewrite /interval; set_tac. move => e. by rewrite -(interval_bag_edge_cover). apply: disjointsU. exact: bag_edges_disj. rewrite disjoint_sym interval_edges_sym. exact: interval_bag_edges_disj. move => x A B. rewrite inE (disjointFl (bag_disj conn_G _ _ Dio)) //= interval_sym in A. exact: (@bag_interval_cap G) B A. 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)