proposition: Lemma plane_emb_arity2 (d : emb_map g) : 1 < arity d.
proof: Proof. apply: loopless_arity. apply: plane_emb_plain. apply: plane_emb_loopless. 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)