proposition: Lemma bin_ffactd n m : 'C(n, m) = n ^_ m %/ m`!.
proof: Proof. by rewrite -bin_ffact mulnK ?fact_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)