proposition: Lemma binom_monotone2 k n m: natp k -> natp n -> natp m -> k <> \0c -> k <=c (csucc n) -> k <=c (csucc m) -> (n <c m <-> (binom n k) <c (binom m k)).
proof: Proof. move=> kN nN mN r1 r2 r3. split; first by apply: binom_monotone1. case: (cleT_el (CS_nat mN) (CS_nat nN)) => // mn [ble bne]. case: (equal_or_not m n) => nm; first by case: bne; rewrite nm. have bgt: (binom m k) <c (binom n k) by apply: binom_monotone1. case:(cltNge bgt ble). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)