proposition: Lemma cprod_Meqlt a b b': natp a -> natp b' -> b <c b' -> a <> \0c -> (a *c b) <c (a *c b').
proof: Proof. move => aN b'N lt anz; move: (NS_lt_nat lt b'N) => bN. move: (card_ltP1 b'N lt) => [c [cN cnz <-]]. rewrite cprodDr; apply:(csum_M0lt (NS_prod aN bN) (cprod2_nz anz cnz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)