proposition: Theorem summation_aux_summation_aux_mul_swap : ∀ g₁ g₂ g₃ b₁ b₂ len, (summation_aux r b₁ len (λ i, summation_aux r b₂ (g₁ i) (λ j, g₂ i * g₃ i j)) = summation_aux r b₁ len (λ i, g₂ i * summation_aux r b₂ (g₁ i) (λ j, g₃ i j)))%K.
proof: Proof. intros g₁ g₂ g₃ b₁ b₂ len. revert b₁ b₂. induction len; intros; [ reflexivity | simpl ]. rewrite IHlen. apply rng_add_compat_r. apply summation_aux_mul_swap. Qed.
imports: Utf8 QArith NPeano Misc Field2