proposition: Lemma del_node_planar (G : hypermap) (z : G) : planar G -> planar (del_node z).
proof: Proof. apply: sub_planar; last by move => x; rewrite val_frestrict. case => x Nx /=. rewrite skip1 // unfold_in -fclosed1 //. exact/closure_closed/cedgeC. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)