proposition: Lemma cprod_M1lt a b: natp a -> a <> \0c -> \1c <c b -> a <c (a *c b).
proof: Proof. move => aN anz lt1b; move: a aN anz; apply: Nat_induction => //. move => n nN hrec _; rewrite cprodC (cprod_via_sum _ (CS_nat nN)) cprodC. case: (equal_or_not n \0c) => h. by rewrite h succ_zero cprod0l (csum0l (proj32_1 lt1b)). move: (csum_Mlteq NS1 (hrec h));rewrite -(Nsucc_rw nN) => h2. by apply:(clt_leT h2); apply:(csum_Meqle _ (proj1 lt1b)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)