proposition: Lemma le_genus_WalkupF (G : hypermap) (x : G) : genus (WalkupF x) <= genus G.
proof: Proof. by rewrite genus_permN -[X in _ <= X]genus_permF le_genus_WalkupE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)