proposition: Lemma loopless_arity (G : hypermap) : plain G -> loopless G -> forall x : G, 1 < arity x.
proof: Proof. move=> plainG llG; apply/forallP; apply: contraNT llG. case/forallPn => x; rewrite -leqNgt => ar_le_1. have ar1 : arity x = 1 by apply/eqP; rewrite eqn_leq ar_le_1 order_gt0. have := iter_face_arity x; rewrite ar1 /= => fx. existsb x. by rewrite -plain_eq' // fx -cnode1r. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)