proposition: Lemma cdivides_smaller a b: b %|c a -> a <> \0c -> b <=c a.
proof: Proof. move => ha. rewrite (cdivides_pr ha) => hb. case: (equal_or_not (a %/c b) \0c) => qz. by case: hb; rewrite qz cprod0r. apply: (cprod_M1le (CS_nat (proj32 ha)) qz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)