proposition: Lemma exponent_pX1p2n n : prime p -> odd p -> exponent p^{1+2*n} = p.
proof: Proof. move=> p_pr odd_p; apply: prime_nt_dvdP => //. rewrite -dvdn1 -trivg_exponent -cardG_gt1 card_pX1p2n //. by rewrite (ltn_exp2l 0) // prime_gt1. elim: n => [|n IHn]. by rewrite (dvdn_trans (exponent_dvdn _)) ?card_pX1p2n. case: pX1p2S => gz isoZ; rewrite -im_cpair /=. apply/exponentP=> xy; case/imset2P=> x y C1x C2y ->{xy}. rewrite expgMn; last by red; rewrite -(centsP (im_cpair_cent isoZ)). rewrite (exponentP _ y C2y) ?exponent_injm ?injm_cpair1g // mulg1. by rewrite (exponentP _ x C1x) ?exponent_injm ?injm_cpairg1 // exponent_pX1p2. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism presentation) mathcomp(quotient action commutator gproduct gfunctor) mathcomp(ssralg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule matrix maximal) mathcomp(extremal)