proposition: Lemma arity_face x : arity (face x) = arity x.
proof: Proof. exact: (arity_iter_face 1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)