proposition: Lemma pack_add_edge (G : pre_graph) (x y : VT) u (isG : is_graph G) (isG' : is_graph (G ∔ [x, u, y])) : pack (G ∔ [x, u, y]) ≃2 pack G ∔ [pack_v x, u, pack_v y].
proof: Proof. exact: pack_add_edge' freshP. Defined.
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)