proposition: Lemma prime_dvd_bin k p : prime p -> 0 < k < p -> p %| 'C(p, k).
proof: Proof. move=> p_pr /andP[k_gt0 lt_k_p]. suffices /Gauss_dvdr<-: coprime p (p - k) by rewrite -mul_bin_down dvdn_mulr. by rewrite prime_coprime // dvdn_subr 1?ltnW // gtnNdvd. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)