proposition: Lemma plain_face (D : hypermap) (x : D) : plain D -> face x = finv node (edge x).
proof: Proof. by move=> plainD; rewrite -plain_eq' // finv_f. 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)