Skip to content

Instantly share code, notes, and snippets.

@huitseeker
Created April 29, 2011 16:24
Show Gist options
  • Save huitseeker/948567 to your computer and use it in GitHub Desktop.
Save huitseeker/948567 to your computer and use it in GitHub Desktop.
Ideas about generalizing prime_dvd_bin
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment