proposition: Lemma binom_monotone3 n k: natp n -> k <=c n -> ( (binom n k) <=c binom n (csucc k) <-> csucc (cdouble k) <=c n).
proof: Proof. move => nN lkn; move: (NS_diff k nN) (NS_le_nat lkn nN) => dN kN. have skN:= NS_succ kN. have eq1:= (binom_rec1 nN lkn). have aux: csucc k <=c n-c k <-> csucc (cdouble k) <=c n. rewrite cdoubleE - (csum_Sn _ kN) - {2} (cdiff_pr lkn) csumC. by split => hyp; [ apply: csum_Meqle|apply: (csum_le2l kN skN dN)]. move: (NS_binom nN kN)(NS_binom nN skN) => b1N b2N. split. move => hyp;apply/aux. move: (cprod_Meqle (n -c k) hyp); rewrite eq1. apply /(cprod_le2r b2N skN dN); apply: (binom_pr3 nN skN). apply/(cleSltP kN); split => // ekn. move: hyp; rewrite ekn (binom_nn nN) (binom_bad nN (NS_succ nN) (cltS nN)). exact: (cltNge clt_01). move/aux => hyp. case: (equal_or_not (n -c k) \0c) => kn. by case: (cltNge(succ_positive k)); rewrite - kn. apply: (cprod_le2l dN b1N b2N kn). by rewrite eq1; apply:cprod_Mleeq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)