proposition: Lemma mul_Sm_binom_1 n p : natp n -> natp p -> n *c (binom (n +c p) p) = (csucc p) *c binom (n+c p) (csucc p).
proof: Proof. move => nN pN. case: (equal_or_not n \0c) => nz. rewrite nz (csum0l (CS_nat pN)) (binom_bad pN (NS_succ pN) (cltS pN)). by rewrite cprod0l cprod0r. rewrite (binom_symmetric2 nN pN). move: (cpred_pr nN nz); set k := cpred n; move => [kN ->]. rewrite (csum_Sn _ kN). rewrite - (mul_Sm_binom kN (NS_sum kN pN)). rewrite - (mul_Sm_binom pN (NS_sum kN pN)). by rewrite (binom_symmetric2 kN pN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)