proposition: Theorem series_mul_add_distr_r : ∀ a b c, ((a + b) * c = a * c + b * c)%ser.
proof: Proof. intros a b c. rewrite series_mul_comm, series_mul_add_distr_l. rewrite series_mul_comm. apply series_add_compat_l. apply series_mul_comm. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation