proposition: Lemma binom_pr1 n p: natp n -> natp p -> p <=c n -> binom n p = (factorial n) %/c ((factorial p) *c (factorial (n -c p))).
proof: Proof. by move=> nN pN h; move: (binom_pr0 nN pN h)=> [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)