proposition: Lemma fitp_rot n p : n <= size_part p -> forall x, exact_fitp x p = exact_fitp (iter n face x) (rot_part n p).
proof: Proof. move=> le_n_p x; rewrite /exact_fitp size_rot_part arity_iter_face. case: eqP => //= nFx. rewrite /rot_part -{1}(cat_take_drop_part n p) !fitp_cat andbC. congr (_ && _); congr (fitp _ _). congr (iter _ face x); move: (congr1 size_part (cat_take_drop_part n p)). by rewrite -(subnKC le_n_p) size_cat_part size_drop_part; apply: addIn. by rewrite -iterD size_drop_part subnK // -nFx iter_face_arity. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)