proposition: Lemma iter_face_arity x : iter (arity x) face x = x.
proof: Proof. exact/iter_order/faceI. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)