proposition: Lemma pfactor_coprime p n : prime p -> n > 0 -> {m | coprime p m & n = m * p ^ logn p n}.
proof: Proof. move=> p_pr n_gt0; set k := logn p n. have dv_pk_n: p ^ k %| n by rewrite pfactor_dvdn. exists (n %/ p ^ k); last by rewrite divnK. rewrite prime_coprime // -(@dvdn_pmul2r (p ^ k)) ?expn_gt0 ?prime_gt0 //. by rewrite -expnS divnK // pfactor_dvdn // ltnn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)