proposition: Lemma expand_parallel (G : pre_graph) (isG : is_graph G) (x y : VT) (e1 e2 : ET) u v : e1 != e2 -> is_edge G e1 x u y -> is_edge G e2 x v y -> pack G ≃2 pack (G - [fset e1; e2]) ∔ [pack_v x, u, pack_v y] ∔ [pack_v x, v, pack_v y].
proof: Proof. Proof with eauto with vset. move => e1De2 edge_e1 edge_e2. symmetry. pose G' := ((G - [fset e1; e2]) ∔ [e1, x, u, y])%O. have isG' : is_graph G'. { apply: add_edge_graph'... } apply: iso2_comp. apply: add_edge2_iso. apply: iso2_sym. unshelve eapply (pack_add_edge' (e := e1)). { abstract (by rewrite !inE eqxx). } rewrite /=. have E : (G - [fset e1; e2]) ∔ [e1, x, u, y] ∔ [e2,x, v,y] ≡G G. { rewrite fsetUC -remove_edges_edges !remove_edgeK //. apply: is_edge_remove_edges edge_e1. by rewrite inE. } apply: iso2_comp (iso2_sym _) _. rewrite -/G'. set Cx := pack_v x. set Cy := pack_v y. have -> : Cx = (pack_v G' x). { rewrite /Cx /G' !pack_vE... move => ? ?. exact: val_inj. } have -> : Cy = (pack_v G' y). { rewrite /Cy /G' !pack_vE... move => ? ?. exact: val_inj. } unshelve eapply (pack_add_edge' (G := G') (e := e2)). - rewrite /G'. symmetry in E. apply: eqvG_graph E. - by rewrite !inE eqxx eq_sym (negbTE e1De2). - exact: eqvG_pack E. Qed.
imports: Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(rewriting open_confluence finmap_plus)