proposition: Lemma le_genus_planar (D D' : hypermap) : genus D' <= genus D -> planar D -> planar D'.
proof: Proof. rewrite /planar -!leqn0. exact: leq_trans. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)