proposition: Lemma ffact_fact n m : natp n -> natp m -> m <=c n -> n ^_c m *c factorial (n -c m) = factorial n.
proof: Proof. move => nN; move: n nN m; apply: Nat_induction. by move => m mN /cle0 ->; rewrite cdiff_0n ffactn0 factorial0 (cprod1r CS1). move => n nN Hrec m mN. have snN := (NS_succ nN). case: (equal_or_not m \0c) => mz. by rewrite mz ffactn0 (cdiff_n0 snN) (cprod1l (CS_nat(NS_factorial snN))). move:(cpred_pr mN mz) => [pN ->]. move/(cleSSP (CS_nat pN) (CS_nat nN)) => lemn. rewrite (cdiff_pr6 nN pN) (ffactnS snN pN) (cpred_pr2 nN) - cprodA. by rewrite (Hrec _ pN lemn) cprodC factorial_succ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)