proposition: Lemma consttX pi x n : (x ^+ n).`_pi = x.`_pi ^+ n.
proof: Proof. elim: n => [|n IHn]; first exact: constt1. by rewrite !expgS consttM ?IHn //; apply: commuteX. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)