proposition: Lemma adjn_irrefl : irreflexive (@adjn D).
proof: Proof. move => x. by rewrite (emb_edge emb_f) sgP. 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)