proposition: Lemma ffact_factd n m : natp n -> natp m -> m <=c n -> n ^_c m = (factorial n) %/c factorial (n -c m).
proof: Proof. move => nN mN le; move: (NS_diff m nN) => dN. move: (NS_factorial dN) (NS_ffact nN mN) => qa qb. by rewrite -(ffact_fact nN mN le) cprodC (cdivides_pr4 qa qb (factorial_nz dN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)