proposition: Lemma add_edge_plain : plain G -> plain H.
proof: Proof. move=> plainG; apply/plainP => -[||z] _ //=. by rewrite (rwP eqP) !inj_eq // plain_eq // plain_neq. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)