proposition: Lemma mul_Sm_binm_1 n p: n * 'C(n+p,p) = p.+1 * 'C(n+p,p.+1).
proof: Proof. case: n => [| n]; first by rewrite add0n mul0n bin_small // muln0. rewrite -binom_mn_n addSn -mul_bin_diag -mul_bin_diag binom_mn_n //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)