proposition: Lemma big_nat_mul n k F : \big[*%M/1]_(0 <= i < n * k) F i = \big[*%M/1]_(0 <= i < n) \big[*%M/1]_(i * k <= j < i.+1 * k) F j.
proof: Proof. elim: n => [|n ih]; first by rewrite mul0n 2!big_nil. rewrite [in RHS]big_nat_recr//= -ih mulSn addnC [in LHS]/index_iota subn0 iotaD. rewrite big_cat /= [in X in _ = X * _]/index_iota subn0; congr (_ * _). by rewrite add0n /index_iota (addnC _ k) addnK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)