proposition: Lemma cprod_M1lt' a b: natp a -> \1c <=c a -> \1c <c b -> a <c a *c b.
proof: Proof. move => aN la lb. have anz:=(nesym (proj2 (clt_leT clt_01 la))). apply:(cprod_M1lt aN anz lb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)