proposition: Lemma expand_pendant (G : pre_graph) (x z : VT) (e : ET) (isG : is_graph G) (Hz : z \notin pIO G) u : edges_at G z = [fset e] -> is_edge G e x u z -> x != z -> pack G ≃2 pack (G \ z) ∔ lv G z ∔ [inl (pack_v x), u, inr tt].
proof: Proof. Proof with eauto with vset. move => Iz arc_e xDz. symmetry. apply: iso2_comp. apply: add_edge2_iso. apply: iso2_sym. apply: pack_add_vertex. instantiate (1 := z). abstract (by rewrite !inE eqxx). rewrite /=. set G' := ((_ \ _) ∔ [_,_])%O. set Sx := Sub _ _. set Sz := Sub _ _. have -> : Sx = (pack_v G' x). { apply: val_inj => /=. rewrite !pack_vE /G' //... } have -> : Sz = (pack_v G' z). { apply: val_inj => /=. rewrite !pack_vE //... by rewrite !inE eqxx. } apply: iso2_comp (iso2_sym _) _. unshelve eapply (pack_add_edge' (e := e)). - apply: add_edge_graph'; rewrite /G'... - by rewrite /G' /= in_fsetD Iz !inE eqxx. - rewrite /G' {}/Sz {}/Sx. apply eqvG_pack. rewrite remove_vertexK ?Iz ?remove_edgeK //... 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)