proposition: Lemma mul_Sm_binm_2 n k: (n-k) * 'C(n,k) = k.+1 * 'C(n,k.+1).
proof: Proof. by have:= (mul_Sm_binm_r n k 1);rewrite !ffactn1 addn1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)