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