proposition: Lemma bin_ffact n m : 'C(n, m) * m`! = n ^_ m.
proof: Proof. have [lt_n_m | le_m_n] := ltnP n m; first by rewrite bin_small ?ffact_small. by rewrite ffact_factd // -(bin_fact le_m_n) mulnA mulnK ?fact_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)