proposition: Lemma dvdn_pfactor p d n : prime p -> reflect (exists2 m, m <= n & d = p ^ m) (d %| p ^ n).
proof: Proof. move=> p_pr; have pn_gt0: p ^ n > 0 by rewrite expn_gt0 prime_gt0. apply: (iffP idP) => [dv_d_pn|[m le_m_n ->]]; last first. by rewrite -(subnK le_m_n) expnD dvdn_mull. exists (logn p d); first by rewrite -(pfactorK n p_pr) dvdn_leq_log. have d_gt0: d > 0 by apply: dvdn_gt0 dv_d_pn. case: (pfactor_coprime p_pr d_gt0) => q co_p_q def_d. rewrite [LHS]def_d ((q =P 1) _) ?mul1n // -dvdn1. suff: q %| p ^ n * 1 by rewrite Gauss_dvdr // coprime_sym coprimeXl. by rewrite muln1 (dvdn_trans _ dv_d_pn) // def_d dvdn_mulr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)