proposition: Lemma Series_plus (a b : nat -> R) : ex_series a -> ex_series b -> Series (fun n => a n + b n) = Series a + Series b.
proof: Proof. intros Ha Hb. replace (Series a + Series b) with (real (Series a + Series b)) by auto. apply (f_equal real), is_lim_seq_unique. apply: is_series_plus ; by apply Series_correct. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy