proposition: Lemma arity3 (x : G) : 2 < arity x.
proof: Proof. Proof using llG plainG deg2 simple. rewrite 1!ltn_neqAle ltnNge [2 != _]rwT /=. - have:= loopless_face x plainG llG. apply: contraNN => /card_le1_eqP /(_ x) A. by rewrite [face x]A // inE -?cface1r. - move/negbT/simple : (deg2 (face x)); rewrite -cnode1 connect0 => /(_ isT). apply: contraNneq => ar2; rewrite faceK -plain_eq' // -cnode1r. by rewrite -[face _]/(iter 2 face x) ar2 iter_face_arity. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)