proposition: Lemma sub_planar : planar G -> planar H.
proof: Proof. rewrite /planar -!leqn0; exact/leq_trans/sub_genus. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)