proposition: Lemma is_series_plus (a b : nat -> V) (la lb : V) : is_series a la -> is_series b lb -> is_series (fun n => plus (a n) (b n)) (plus la lb).
proof: Proof. move => Ha Hb. apply filterlim_ext with (fun n => plus (sum_n a n) (sum_n b n)). elim => [ | n IH]; simpl. by rewrite !sum_O. rewrite !sum_Sn -IH; rewrite <- 2!plus_assoc; apply f_equal. rewrite 2!plus_assoc; apply f_equal2; try easy. apply plus_comm. now apply filterlim_comp_2 with (3 := filterlim_plus _ _). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy