proposition: Lemma binom_monotone_max_arg n k (h := chalf n): natp n -> k <=c n -> ( (binom n k) = (binom n h) <-> (k = h \/ n -c k = h) ).
proof: Proof. move => nN lkn. have hN:= (NS_half nN). split; last first. case; move <- => //; exact: (binom_symmetric nN lkn). wlog ll : k lkn/ (k <=c h). move => hyp; move: (NS_le_nat lkn nN) => kN. case:(NleT_el kN hN); first by apply: hyp. rewrite (binom_symmetric nN lkn) => lt1 eq1. have qa: n -c k <=c h. move/(cleSltP hN): lt1 => /(csum_Meqle (chalf n)) => le. apply:(cdiff_Mle hN kN); apply: (cleT _ le). rewrite (csum_nS _ hN) - cdoubleE. case: (cdouble_halfV nN) => <-; fprops. move: (cleT qa (cle_halfn_n nN)) => qb. case: (hyp (n -c k) qb qa eq1); [by right | move <-; left ]. by rewrite double_diff. move: (NS_le_nat lkn nN) => kN. case:(cle_eqVlt ll); first by left. move/(cleSltP kN) => lskh rq1. move: (cleT lskh (cle_halfn_n nN)) => lskn. move: (half_monotone2 (NS_succ kN) nN lskh) => /(binom_monotone4 nN lkn) le3. by case: (proj2(clt_leT le3 (binom_max nN lskn))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)