proposition: Lemma cycleG' : forall x y : G , x != y -> cnode x y -> ~~ cface (edge x) (edge y).
proof: Proof. move => x y xDy; apply: contraTN; rewrite cface1 cface1r => /cycleG. rewrite (inj_eq faceI) (inj_eq edgeI) => /(_ xDy). by rewrite cnode1 cnode1r !edgeK. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)