proposition: Lemma add_edge1n_diso_proof (G : sgraph) (A : {set G}) (x y : G) : @add_edges2_rel (add_edge G x y) [set x] A =2 add_edges2_rel _ [set x] (y |: A).
proof: Proof. move=> u v. rewrite /= !inE /edge_rel/= /edge_rel /=. case (sedge _ _) => //=. case: (eqVneq u v) => H; subst => //=. case: (eqVneq u x) => ?; subst => //=. all: case: (eqVneq v x) => ?; subst => //=. by rewrite eqxx in H. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)