proposition: Lemma adjn_face (x : D) : adjn x (face x).
proof: Proof. apply/exists_inP; exists x; first exact: connect0. rewrite in_applicative -plain_eq' -?cnode1r ?connect0 //. exact: emb_plain emb_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)