proposition: Theorem convol_mul_add_distr_l : ∀ a b c i, (convol_mul a (b + c)%ser i = convol_mul a b i + convol_mul a c i)%K.
proof: Proof. intros a b c k. unfold convol_mul. rewrite <- summation_add_distr. apply summation_compat; intros i Hi. rewrite series_nth_add. rewrite rng_mul_add_distr_l. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation