proposition: Lemma seriesD (V : zmodType) (f g : V ^nat) : series (f + g) = series f + series g.
proof: Proof. by rewrite /series /= funeqE => n; rewrite big_split. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau