proposition: Lemma merge_add_edgeLE G H x y u l i o z: @merge_add_edgeL G H x y u l i o (\pi z) = (\pi z).
proof: Proof. rewrite /merge_add_edgeL/=. rewrite (@merge_isoE _ _ _ _ (union_add_edge_l H x u y) l). rewrite merge_add_edgeE. by rewrite merge_sameE. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2 rewriting)