proposition: Lemma genus_walkupN_eq (G : hypermap) (z : G) : ~~ cnode z (face z) -> genus (WalkupN z) = genus G.
proof: Proof. move => ncross. rewrite /WalkupN genus_permF genus_WalkupE_eq ?genus_permN //. by right. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)