proposition: Lemma edges_replace (G : pre_graph) (z z' : VT) (e1 e2 e2' : ET) (x : VT) (u : tm) : edges_at G z = [fset e1; e2] -> edges_at G z' = [fset e2; e2'] -> e1 != e2 -> e2 != e2' -> e1 != e2' -> edges_at ((G \ z) ∔ [maxn e1 e2, x, u, z']) z' = [fset maxn e1 e2; e2'].
proof: Proof. move => Iz Iz' /negbTE E1 /negbTE E2 /negbTE E3. rewrite edges_at_add_edge /= ?Iz ?maxn_fsetD //. suff -> : edges_at (G \ z) z' = [fset e2'] by []. rewrite edges_at_del Iz Iz'. apply/fsetP => e. rewrite !inE negb_or -andbA. apply/and3P/idP => [[A B /orP [/eqP C|/eqP C]]|/eqP->] ; subst. - by rewrite eqxx in B. - by rewrite eq_sym E3 in A. - by rewrite eqxx orbT eq_sym E3 eq_sym E2. Qed.
imports: HB(structures) Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom rewriting) GraphTheory(finmap_plus)