proposition: Lemma binom_max n k: natp n -> k <=c n -> (binom n k) <=c binom n (chalf n).
proof: Proof. move => nN lkn; move: (NS_half nN) => hN. suff: forall k, k <c chalf n -> binom n k <=c binom n (chalf n). move => hyp. move: (NS_le_nat lkn nN) => kN. case: (NleT_ell hN kN) => sm. + rewrite sm; apply: cleR; apply:(CS_nat (NS_binom nN kN)). + case: (p_or_not_p (oddp n /\ k = csucc (chalf n)))=> sp. move: (binom_half_aux nN (proj1 sp)); rewrite - (proj2 sp) => ->. by apply:(cleR (CS_nat (NS_binom nN kN))). rewrite (binom_symmetric nN lkn); apply: hyp;apply:(cdiff_Mlt hN nN lkn). case: (p_or_not_p (evenp n)) => nev. apply: (cle_ltT _ (csum_Meqlt hN sm)). rewrite csum_nn -/(cdouble _) - (half_even nev);fprops. have on: oddp n by []. rewrite {1} (half_odd on) cdoubleE -(csum_nS _ hN). apply:(csum_Meqlt hN); split; [ by apply/cleSltP | fprops ]. + by apply: hyp. clear k lkn. move:{1 2 4 5} (chalf n) hN (cleR (CS_nat hN)). apply: Nat_induction. by move => _ k /clt0. move =>m mN Hrec mp k kl. have cdm: csucc (cdouble m) <=c n. apply: cleT (half_monotone2 (NS_succ mN) nN mp). by rewrite (double_succ mN); apply: cleS; apply: NS_succ; apply: NS_double. have lemn:= (cleT (cleT (cleS mN) mp) (cle_halfn_n nN)). move/(binom_monotone3 nN lemn): cdm. move/(cltSleP mN): kl => /cle_eqVlt; case; [ by move -> | move => lkm]. apply: cleT; exact: (Hrec (cleT (cleS mN) mp) k lkm). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)