proposition: Lemma cprod_Mlelt a b a' b': natp a' -> natp b' -> a <=c a' -> b <c b' -> a' <> \0c -> (a *c b) <c (a' *c b').
proof: Proof. move=> a'N b'N aa' bb' anz. apply: (cle_ltT (cprod_Mleeq b aa') (cprod_Meqlt a'N b'N bb' anz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)