proposition: Lemma add_edge_planar : cface x y -> planar G -> planar h_add_edge.
proof: Proof. by move=> f_x_y; rewrite /planar add_edge_genus. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)