proposition: Lemma ffactSS n m : natp n -> natp m -> (csucc n) ^_c (csucc m) = (csucc n) *c n ^_c m.
proof: Proof. by move => nN mN; rewrite (ffactnS (NS_succ nN) mN) cpred_pr2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)