proposition: Theorem summation_mul_summation_summation : ∀ g n k, (0 < n)%nat → (0 < k)%nat → (Σ (i = 0, k * n - 1), g i = Σ (i = 0, k - 1), Σ (j = 0, n - 1), g (i * n + j)%nat)%K.
proof: Proof. intros g n k Hn Hk. unfold summation. do 2 rewrite Nat.sub_0_r. destruct n; [ exfalso; revert Hn; apply Nat.lt_irrefl | clear Hn ]. destruct k; [ exfalso; revert Hk; apply Nat.lt_irrefl | clear Hk ]. rewrite Nat.sub_succ, Nat.sub_0_r. rewrite <- Nat.sub_succ_l, Nat.sub_succ, Nat.sub_0_r. rewrite summation_aux_mul_summation_aux_summation_aux. apply summation_aux_compat; intros i Hi. rewrite Nat.sub_succ, Nat.sub_0_r, Nat.sub_0_r. reflexivity. simpl; apply le_n_S, Nat.le_0_l. Qed.
imports: Utf8 QArith NPeano Misc Field2