proposition: Lemma add_node_plain : plain G -> plain h_add_node.
proof: Proof. move/plainP => plain_G; apply/plainP => -[||z] //= _. by move/(_ z isT) : plain_G => [-> ->]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)