proposition: Lemma seriesN (V : zmodType) (f : V ^nat) : series (- f) = - series f.
proof: Proof. by rewrite funeqE => n; rewrite /series /= sumrN. 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