proposition: Lemma binom_pr3 n p: natp n -> natp p -> p <=c n -> binom n p <> \0c.
proof: Proof. move=> nN pN h bz; move: (binom_good nN pN h). rewrite bz cprod0l => fz. by case: (factorial_nz nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)