proposition: Lemma p_elt_exp pi x m : pi.-elt (x ^+ m) = (#[x]`_pi^' %| m).
proof: Proof. apply/idP/idP=> [pi_xm | /dvdnP[q ->{m}]]; last first. rewrite mulnC; apply: pnat_dvd (part_pnat pi #[x]). by rewrite order_dvdn -expgM mulnC mulnA partnC // -order_dvdn dvdn_mulr. rewrite -(@Gauss_dvdr _ #[x ^+ m]); last first. by rewrite coprime_sym (pnat_coprime pi_xm) ?part_pnat. apply: (@dvdn_trans #[x]); first by rewrite -{2}[#[x]](partnC pi) ?dvdn_mull. by rewrite order_dvdn mulnC expgM expg_order. 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)