proposition: Lemma ffact_prod n m : n ^_ m = \prod_(i < m) (n - i).
proof: Proof. elim: m n => [n | m IH [|n] //]; first by rewrite ffactn0 big_ord0. by rewrite big_ord_recr /= sub0n muln0. by rewrite ffactSS IH big_ord_recl subn0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)