proposition: Lemma cprod_lt2l: (a *c b) <c (a *c c) -> b <c c.
proof: Proof. move=> [abc nac]; case: (equal_or_not a \0c) => anz. by case: nac; rewrite anz !cprod0l. split; [ by apply: cprod_le2l | move => bc;case: nac; ue]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)