proposition: Lemma big_nat_mul (R : zmodType) (f : R ^nat) (n k : nat) : \sum_(0 <= i < n * k) f i = \sum_(0 <= i < n) \sum_(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: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) reals ereal nsatz_realtype signed topology normedtype landau sequences derive realfun exp