proposition: Lemma binom_ffact n m : natp n -> natp m -> binom n m *c (factorial m) = n ^_c m.
proof: Proof. move => nN mN. case: (NleT_el mN nN) => cnm; last first. by rewrite (binom_bad nN mN cnm) (ffact_small mN cnm) cprod0l. move:(binom_good nN mN cnm). rewrite - (ffact_fact nN mN cnm) cprodA. have ha := (NS_factorial (NS_diff m nN)). have hb := (NS_prod (NS_binom nN mN) (NS_factorial mN)). apply: (cprod_eq2r ha hb (NS_ffact nN mN) (factorial_nz (NS_diff m nN))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)