proposition: Lemma actXin x a i : a \in D -> to x (a ^+ i) = iter i (to^~ a) x.
proof: Proof. move=> Da; elim: i => /= [|i <-]; first by rewrite act1. by rewrite expgSr actMin ?groupX. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)