proposition: Lemma mul_Sm_binm_r n k p: (n-k) ^_ p * 'C(n,k) = (k +p) ^_ p * 'C(n,k+p).
proof: Proof. move: k;elim:p => [k | p IHp k]; first by rewrite !ffactn0 addn0. have aux: (n-k) * 'C(n,k) = k.+1 * 'C(n,k.+1). case(leqP k n) => h; first by rewrite -{2 3}(subnK h) -mul_Sm_binm_1. by rewrite bin_small // bin_small // ? muln0 // leqW. rewrite 2!ffactnS (mulnC (n-k)) -mulnA aux mulnCA - subnS IHp {IHp}. rewrite mulnA addnS -addSn; congr (_ * _). case: p; [ by rewrite addn0 | move => p]. by rewrite ffactnS mulnCA addnS succnK ffactnSr addnK (mulnC _ k.+1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)