proposition: Lemma big_nat_recr n m F : m <= n -> \big[*%M/1]_(m <= i < n.+1) F i = (\big[*%M/1]_(m <= i < n) F i) * F n.
proof: Proof. by move=> lemn; rewrite (@big_cat_nat n) ?leqnSn // big_nat1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)