proposition: Lemma ffactnS n m : natp n -> natp m -> n ^_c (csucc m) = n *c (cpred n) ^_c m.
proof: Proof. move => nN mN. move: m mN n nN; apply: Nat_induction. by move => n nN; rewrite ffactn0 succ_zero (ffactn1 nN) (cprod1r (CS_nat nN)). move => m mN Hrec n nN. rewrite (ffactnSr _ mN) (ffactnSr _ (NS_succ mN)). rewrite (Hrec n nN) - cprodA. case: (equal_or_not n \0c) => nz; first by rewrite nz !cprod0l. by move: (cpred_pr nN nz) => [qa qb]; rewrite {3} qb cdiff_pr6. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)