proposition: Lemma add_node_planar : planar h_add_node = planar G.
proof: Proof. by rewrite /planar add_node_genus. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)