proposition: Lemma fact_split n m : m <= n -> n`! = m`! * \prod_(m.+1 <= k < n.+1) k.
proof: Proof. by move=> leq_mn; rewrite !fact_prod -big_cat_nat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)