proposition: Lemma dvdn_pexp2r m n k : k > 0 -> (m ^ k %| n ^ k) = (m %| n).
proof: Proof. move=> k_gt0; apply/idP/idP=> [dv_mn_k|]; last exact: dvdn_exp2r. have [->|n_gt0] := posnP n; first by rewrite dvdn0. have [n' def_n] := dvdnP (dvdn_gcdr m n); set d := gcdn m n in def_n. have [m' def_m] := dvdnP (dvdn_gcdl m n); rewrite -/d in def_m. have d_gt0: d > 0 by rewrite gcdn_gt0 n_gt0 orbT. rewrite def_m def_n !expnMn dvdn_pmul2r ?expn_gt0 ?d_gt0 // in dv_mn_k. have: coprime (m' ^ k) (n' ^ k). rewrite coprime_pexpl // coprime_pexpr // /coprime -(eqn_pmul2r d_gt0) mul1n. by rewrite muln_gcdl -def_m -def_n. rewrite /coprime -gcdn_modr (eqnP dv_mn_k) gcdn0 -(exp1n k). by rewrite (inj_eq (expIn k_gt0)) def_m; move/eqP->; rewrite mul1n dvdn_gcdr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)