proposition: Lemma binom_monotone1 k n m: natp k -> natp n -> natp m -> k <> \0c -> k <=c (csucc n) -> n <c m -> (binom n k) <c (binom m k).
proof: Proof. move: k n m. have : forall k n, natp k -> natp n -> k <> \0c -> k <=c (csucc n) -> (binom n k) <c (binom (csucc n) k). move => k n kN nN r1 r2. move: (cpred_pr kN r1) => [pN ps]. rewrite {2} ps (binomSnSm nN pN) -ps. apply: (csum_M0lt (NS_binom nN kN));apply: binom_pr3 =>//. apply /(cleSSP (CS_nat pN) (CS_nat nN)); rewrite -ps//. move=> aux k n m kN nN mN r1 r2 r3. move/(cleSltP nN): r3 => r6. have r8:= cleR (CS_nat mN). pose r p := (binom n k) <c (binom p k). apply: (Nat_induction3 (r:=r) (NS_succ nN) mN (aux _ _ kN nN r1 r2) _ r6 r8). move => n' r4 r5 r7;apply:(clt_ltT r7). apply: (aux _ _ kN (NS_lt_nat r5 mN) r1). exact:(cleT (cleT r2 r4) (cleS0 (proj32 r4))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)