proposition: Lemma actZr x n : {morph actr^~ x : u / u *+ n}.
proof: Proof. by move=> u; elim: n => [|n IHn]; rewrite ?act0r // !mulrS actAr IHn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype bigop ssralg finset fingroup) mathcomp(morphism perm finalg action gproduct commutator) mathcomp(cyclic)