proposition: Lemma cprod_ge1 a b: natp a -> natp b -> \1c <=c a *c b -> (\1c <=c a) /\ (\1c <=c b).
proof: Proof. move => aN bN pg1. have pnz:=(proj2 (clt_leT clt_01 pg1)). case: (equal_or_not a \0c) => az; first by case: pnz; rewrite az cprod0l. case: (equal_or_not b \0c) => bz; first by case: pnz; rewrite bz cprod0r. by split; apply: cge1 => //; apply CS_nat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)