proposition: Lemma mul_bin_down n m : n * 'C(n.-1, m) = (n - m) * 'C(n, m).
proof: Proof. case: n => //= n; have [lt_n_m | le_m_n] := ltnP n m. by rewrite (eqnP lt_n_m) mulnC bin_small. by rewrite -!['C(_, m)]bin_sub ?leqW ?subSn ?mul_bin_diag. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)