proposition: Lemma cprod_le2l: a <> \0c -> (a *c b) <=c (a *c c) -> b <=c c.
proof: Proof. move=>naz abc; case: (NleT_el bN cN) => // ltcb. case: (cleNgt abc (cprod_Meqlt aN bN ltcb naz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)