proposition: Lemma merge_add_edgeL (G H : graph) x y u l i o : point (merge_seq (G ∔ [x,u,y] ⊎ H) l) (\pi i) (\pi o) ≃2 point (merge_seq (G ⊎ H) l) (\pi i) (\pi o) ∔ [\pi inl x,u,\pi inl y].
proof: Proof. eapply iso2_comp. apply (iso_iso2' (h:=merge_iso (union_add_edge_l _ _ _ _) _)). 1,2: by rewrite merge_isoE. eapply iso2_comp. refine (iso_iso2' (h:=merge_add_edge _ _ _ _) _ _). 1,2: by rewrite merge_add_edgeE. unshelve refine (iso_iso2' (h:=add_edge_iso'' (h:=mgraph.merge_same _) _ _ _) _ _)=>/=. 4: reflexivity. by rewrite map_pairs_id. all: by rewrite merge_sameE. Defined.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2 rewriting)