proposition: Lemma emb_arity3 (x : D) : (forall y, 1 < #|N(f y)|) -> 2 < arity x.
proof: Proof. move => deg2. apply: arity3 => //;[exact: emb_plain emb_f|exact: emb_loopless|]. move=> {x} x. apply: contraTF (deg2 x); rewrite -leqNgt => /eqP nxx. apply: leq_trans (emb_degree _) _. exact: order_le_fix. 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)