proposition: Theorem summation_mul_comm : ∀ g h b k, (Σ (i = b, k), g i * h i = Σ (i = b, k), h i * g i)%K.
proof: Proof. intros g h b len. apply summation_compat; intros i Hi. apply rng_mul_comm. Qed.
imports: Utf8 QArith NPeano Misc Field2