proposition: Lemma porbit_mod s x i : (s ^+ i)%g x = (s ^+ (i %% #|porbit s x|))%g x.
proof: Proof. Proof using. rewrite {1}(divn_eq i #|porbit s x|) expgD permM; congr aperm. elim: (i %/ #|porbit s x|) => [| {}i IHi]. - by rewrite mul0n expg0 perm1. - by rewrite mulSnr expgD permM IHi permX; exact: iter_porbit. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action ssralg) tools permcomp