proposition: Lemma binom_ffactd n m : natp n -> natp m -> binom n m = n ^_c m %/c (factorial m).
proof: Proof. move => nN mN. have ha := (NS_factorial mN). have hb := NS_binom nN mN. by rewrite -(binom_ffact nN mN) cprodC (cdivides_pr4 ha hb (factorial_nz mN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)