proposition: Lemma binom_monotone4 n k: natp n -> k <=c n -> ( (binom n k) <c binom n (csucc k) <-> cdouble (csucc 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 qa: natp (csucc (cdouble k)) by apply:NS_succ; apply:NS_double. have: csucc (cdouble k) <c n <-> cdouble (csucc k) <=c n. rewrite (double_succ kN); apply: iff_sym; exact:(cleSltP qa). have b1N: natp (binom n k) by apply: NS_binom. have b2N: natp (binom n (csucc k)) by apply: NS_binom. apply: iff_trans; split. move => [/(binom_monotone3 nN lkn) h neq]; split => // eq2. have eq3 :csucc k = (n -c k). by rewrite - eq2 cdoubleE - (csum_Sn _ kN) cdiff_pr1. by case: neq; apply: (cprod_eq2l skN b1N b2N (@succ_nz _)); rewrite - eq1 eq3. move => [/(binom_monotone3 nN lkn) le1 neq]; split => // eq2. move/(strict_pos_P1 b1N): (binom_pr3 nN kN lkn) => lt1. move: (nesym (proj2(clt_leT lt1 le1))) => bnz. rewrite eq2 in eq1. move:(cprod_eq2r b2N dN skN bnz eq1) => nk. case: neq; rewrite -(cdiff_pr lkn) nk (csum_nS _ kN) csum_nn //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)