proposition: Lemma pfactor_dvdn p n m : prime p -> m > 0 -> (p ^ n %| m) = (n <= logn p m).
proof: Proof. move=> p_pr; elim: n m => [|n IHn] m m_gt0; first exact: dvd1n. rewrite lognE p_pr m_gt0 /=; case dv_pm: (p %| m); last first. apply/dvdnP=> [] [/= q def_m]. by rewrite def_m expnS mulnCA dvdn_mulr in dv_pm. case/dvdnP: dv_pm m_gt0 => q ->{m}; rewrite muln_gt0 => /andP[p_gt0 q_gt0]. by rewrite expnSr dvdn_pmul2r // mulnK // IHn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)