proposition: Lemma genus_gt0 (D : hypermap) : (0 < genus D) = (0 < Euler_lhs D - Euler_rhs D).
proof: Proof. by rewrite even_genusP -addnBA // subnn addn0 double_gt0. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)