proposition: Lemma loopless_face (G : hypermap) (x : G) : plain G -> loopless G -> ~~ cnode x (face x).
proof: Proof. move => plFG /existsPn llG. by rewrite cnode1r plain_eq'. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)