proposition: Lemma bin_fact n m : m <= n -> 'C(n, m) * (m`! * (n - m)`!) = n`!.
proof: Proof. elim: n m => [|n IHn] [|m] // le_m_n; first by rewrite bin0 !mul1n. by rewrite !factS -!mulnA mulnCA mulnA -mul_bin_diag -mulnA IHn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)