proposition: Lemma bin_valp m k p : m > 0 -> prime p -> m <= k -> logn p (m * 'C(k, m)) <= logn p (l k).
proof: Proof. move => gt_m_0 prime_p leq_mk. have le2p : 2 <= p by exact: prime_gt1. have gt_k0 : (k > 0) by rewrite (@leq_trans m). set vp := logn p. set tp := trunc_log p. have hvp_bin : vp 'C(k,m) = vp k`! - (vp m`! + vp (k - m)`!). rewrite bin_factd // /vp logn_div ?lognM ?fact_gt0 //. by rewrite -(bin_fact leq_mk) dvdn_mull. have {}hvp_bin : vp 'C(k, m) = \sum_(i < tp k) (k %/ p ^ i.+1) - \sum_(i < tp k) (m %/ p ^ i.+1 + (k - m) %/ p ^ i.+1). rewrite -fact_logp_sum_small ?trunc_log_ltn //. rewrite big_split /= -!fact_logp_sum_small ?trunc_log_ltn //. - by apply: (ltn_trans _ (trunc_log_ltn _ le2p)); rewrite ltn_subrL gt_m_0. - exact: (leq_trans _ (trunc_log_ltn _ le2p)). have {}hvp_bin : vp 'C(k, m) = \sum_(i < tp k - vp m) (k %/ p ^ (vp m + i).+1) - \sum_(i < tp k - vp m) (m %/ p ^ (vp m + i).+1 + (k - m) %/ p ^ (vp m + i).+1). set rhs := RHS; rewrite {}hvp_bin. have -> : tp k = vp m + (tp k - vp m) by rewrite subnKC ?leq_logn_trunc. rewrite 2!big_split_ord /=. set x := \sum_(i < vp m) _; set y := \sum_(i < vp m) _. suff <- : x = y by rewrite subnDl. by apply: eq_bigr => [] [i] Him _ /=; rewrite -divnDl ?subnKC ?pfactor_dvdn. have min_vplk : vp m + (tp k - vp m) <= vp (l k). rewrite -maxnE geq_max. have -> : vp m <= vp (l k) by apply: dvdn_leq_log => //; exact: iter_lcmn_div. suff -> : tp k <= vp (l k) by []. rewrite -pfactor_dvdn //; apply: iter_lcmn_div; last exact: trunc_logP. by rewrite expn_gt0 prime_gt0. suff {min_vplk} h : vp 'C(k, m) <= tp k - vp m. by apply: leq_trans min_vplk; rewrite /vp lognM ?bin_gt0 // leq_add2l. have -> : tp k - vp m = \sum_(i < tp k - vp m) 1 by rewrite sum1_card card_ord. rewrite {}hvp_bin leq_subLR -big_split /=; apply: leq_sum=> [] [i hi] _ /=. have e : k = m + (k - m) by rewrite subnKC. rewrite {}[X in X%/ _]e; exact: leq_divDl. Qed.
imports: mathcomp(all_ssreflect all_algebra)