proposition: Lemma pack_add_edge' (G : pre_graph) e x y u (isG : is_graph G)(isG' : is_graph (G ∔ [e,x, u, y])) : e \notin eset G -> pack (G ∔ [e,x, u, y]) ≃2 pack G ∔ [pack_v x, u, pack_v y].
proof: Proof. move => eG. apply: iso2_sym. iso2 (bij_id) (fresh_bij bij_id eG) (fun => false) => //. 2-3: exact: val_inj. split => //. - move => [e'|] b; apply: val_inj => //. + by rewrite fresh_bijE /= updateE ?fsval_eqF. + rewrite fresh_bijE /= updateE. by case: b; rewrite pack_vK // ?fsval_eqF add_edgeV. - by move => [e'|] /=; rewrite updateE // fsval_eqF. 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)