proposition: Lemma expand_chain (G : pre_graph) (isG : is_graph G) (x y z : VT) (e1 e2 : ET) (Hz : z \notin pIO G) u v : edges_at G z = [fset e1; e2] -> e1 != e2 -> x != z -> y != z -> is_edge G e1 x u z -> is_edge G e2 z v y -> x \in vset G -> y \in vset G -> pack G ≃2p pack (G \ z) ∔ lv G z ∔ [inl (pack_v x), u, inr tt] ∔ [inr tt, v, inl (pack_v y)].
proof: Proof. Proof with eauto with vset. move => Iz e1De2 xDz yDz arc_e1 arc_e2 Vx Vy. symmetry. constructor. apply: iso2_comp. apply: add_edge2_iso. apply: add_edge2_iso. apply: iso2_sym. apply: (@pack_add_vertex (G \ z) _ z _). abstract (by rewrite !inE eqxx). rewrite /=. set G' := add_vertex _ _ _. set Sx := Sub _ _. set Sz := Sub _ _. set Sy := Sub _ _. have -> : Sx = (pack_v G' x). apply: val_inj => /=. rewrite !pack_vE //... rewrite /G'... have -> : Sy = (pack_v G' y). apply: val_inj => /=. rewrite !pack_vE //... rewrite /G'... have -> : Sz = (pack_v G' z). apply: val_inj => /=. rewrite !pack_vE //... rewrite /G'... rewrite {}/G'. clear Sx Sy Sz. have isG' : is_graph ((G \ z) ∔ [z, lv G z] ∔ [e1, x, u, z]). { apply: add_edge_graph'... } apply: iso2_comp. apply: add_edge2_iso. apply: iso2_sym. eapply (pack_add_edge' (e := e1))... { abstract( by rewrite inE negb_and negbK Iz !inE eqxx). } rewrite /=. have C k (Vk : k \in vset G) : pack_v ((G \ z) ∔ [z, lv G z]) k = pack_v ((G \ z) ∔ [z, lv G z] ∔ [e1, x, u, z]) k. { apply: val_inj => /=. rewrite !pack_vE //; rewrite !inE Vk; by case: (k == z). } have ? : z \in vset G by exact: is_edge_vsetR arc_e1. have E: (G \ z) ∔ [z, lv G z] ∔ [e1, x, u, z] ∔ [e2, z, v, y] ≡G G. { rewrite remove_vertexK // Iz fsetUC -remove_edges_edges !remove_edgeK //. apply: is_edge_remove_edges arc_e1. by rewrite !inE e1De2. } rewrite !{}C //... apply: iso2_comp. apply: iso2_sym. eapply (pack_add_edge' (e := e2)). { by rewrite 3!inE Iz eq_sym !inE eqxx. } apply: eqvG_pack E. Unshelve. symmetry in E. exact: eqvG_graph 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)