proposition: Lemma binom_good n m: natp n -> natp m -> m <=c n -> (binom n m) *c ((factorial m) *c (factorial (n -c m))) = (factorial n).
proof: Proof. by move=> nN mN h; move: (binom_alt_pr nN mN); Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)