proposition: Lemma binom_pr0 n p (num := factorial n) (den:= (factorial p) *c (factorial (n -c p))): natp n -> natp p -> p <=c n -> den %|c num /\ binom n p = num %/c den.
proof: Proof. move=> nN pN h; move: (binom_good nN pN h). have nuN: natp num by apply: NS_factorial =>//. have deN: natp den by apply: NS_prod;apply: NS_factorial; fprops. have dnz: den <> \0c. rewrite /den; apply: cprod2_nz; apply: factorial_nz; fprops. have bN: natp (binom n p) by apply: NS_binom =>//. rewrite cprodC -/num => <-. by split; [ apply:cdivides_pr1 |rewrite cdivides_pr4 ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)