proposition: Lemma face_connect dx dy : @cface[D] dx dy -> connect (--) (g dx) (g dy).
proof: Proof. by rewrite -emb_gcomp //; apply: gcompF. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)