proposition: Lemma ffact_factd n m : m <= n -> n ^_ m = n`! %/ (n - m)`!.
proof: Proof. by move/ffact_fact <-; rewrite mulnK ?fact_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)