proposition: Theorem summation_summation_mul_swap : ∀ g₁ g₂ g₃ k, (Σ (i = 0, k), Σ (j = 0, g₁ i), g₂ i * g₃ i j = Σ (i = 0, k), g₂ i * Σ (j = 0, g₁ i), g₃ i j)%K.
proof: Proof. intros g₁ g₂ g₃ k. apply summation_aux_summation_aux_mul_swap. Qed.
imports: Utf8 QArith NPeano Misc Field2