proposition: Theorem summation_aux_mul_summation_aux_summation_aux : ∀ g k n, (summation_aux r 0 (S k * S n) g = summation_aux r 0 (S k) (λ i, summation_aux r 0 (S n) (λ j, g (i * S n + j)%nat)))%K.
proof: Proof. intros g k n. revert n; induction k; intros. simpl; rewrite Nat.add_0_r, rng_add_0_r; reflexivity. remember (S n) as x. remember (S k) as y. simpl; subst x y. rewrite Nat.add_comm. rewrite summation_aux_ub_add, IHk. symmetry; rewrite rng_add_comm. symmetry. rewrite summation_aux_succ_first. rewrite rng_add_shuffle0, rng_add_comm. symmetry. replace (S k) with (k + 1)%nat by fast_omega. rewrite summation_aux_ub_add. rewrite <- rng_add_assoc. apply rng_add_compat_l. simpl. rewrite rng_add_comm. apply rng_add_compat_l. symmetry; rewrite Nat.add_comm; simpl. rewrite Nat.add_0_r, rng_add_0_r. apply rng_add_compat_l. apply summation_aux_compat; intros i Hi; simpl. rewrite Nat.add_succ_r; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2