Ideas about generalizing prime_dvd_bin

prime_dvd_bin_exp,v

Lemma ltn_pfactor : forall n k p, prime p -> 0 < k < p^n -> logn p k < n.
Proof.
move=> n k p p_pr; case/andP=> k_gt0 ltn_k_pn.
by rewrite ltnNge -(pfactor_dvdn n p_pr k_gt0) (gtnNdvd k_gt0 ltn_k_pn).
Qed.

Lemma primek_dvd_bin : forall n k p, prime p -> 0 < k < p^n -> p %| 'C(p^n, k).
Proof.
move=> n k p p_pr gt0kpn; case/andP: (gt0kpn)=> k_gt0 lt_k_pn.
have def_pn := ltn_predK lt_k_pn; have logpk_ltn := (ltn_pfactor p_pr gt0kpn).
have: p^n %| p^n * 'C((p^n).-1, k.-1) by rewrite dvdn_mulr.
rewrite -def_pn mul_Sm_binm def_pn (ltn_predK k_gt0).
have Hnlog := (subnK (ltnW logpk_ltn)); have n_gt0: 0 < n.
  by move: lt_k_pn k_gt0; case n =>//; rewrite expn0 ltnS leqNgt; move/negbTE->.
case:(pfactor_coprime p_pr k_gt0) => m m_cop k_pfac.
rewrite {1}k_pfac -mulnAC -{1}Hnlog expn_add dvdn_pmul2r ?expn_gt0 ?prime_gt0 //.
rewrite gauss; last by rewrite coprime_pexpl =>//; rewrite subn_gt0; apply:ltn_pfactor.
move/dvdnP=>[k0 ->]; move:logpk_ltn; rewrite -subn_gt0.
by move/ltn_predK=><-; rewrite expnS mulnCA dvdn_mulr ?dvdnn.
Qed.