proposition: Lemma fit_hubcap_rot (x : G) p : arity x = nhub -> exact_fitp x p -> forall j, j < nhub -> exact_fitp (iter j face (inv_face2 x)) (hubcap_rot j p).
proof: Proof. move=> nFx fit_xp; have n_gt1: 1 < nhub by rewrite -nFx 3?ltnW ?pentaG. have [/eqP Ep _] := andP fit_xp; rewrite nFx in Ep. case=> [|[|j]] ltjn; rewrite -?iterSr. - rewrite -(iter_face_arity x) nFx -(subnKC n_gt1) /hubcap_rot addn0. by rewrite /inv_face2 /= !faceK -fitp_rot -?Ep ?leq_subr. - rewrite -(iter_face_arity x) nFx -(subnKC (ltnW n_gt1)) /hubcap_rot addn1. by rewrite subSS /inv_face2 /= nodeK faceK -fitp_rot -?Ep ?leq_subr. by rewrite /hubcap_rot !iterSr !nodeK -fitp_rot -?Ep // 3?ltnW. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry quiztree part discharge)