proposition: Theorem series_mul_add_distr_l : ∀ a b c, (a * (b + c) = a * b + a * c)%ser.
proof: Proof. intros a b c. constructor; intros k; simpl. apply convol_mul_add_distr_l. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation