proposition: Lemma add_edge_genus : cface x y -> genus H = genus G.
proof: Proof. move => f_x_y; rewrite (hiso_genus h_add_edge_iso) /G' /H. rewrite genus_WalkupE_eq; last by left. rewrite genus_walkupF_eq //. exact: add_edge_no_cross. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)