proposition: Lemma ex_series_plus (a b : nat -> V) : ex_series a -> ex_series b -> ex_series (fun n => plus (a n) (b n)).
proof: Proof. move => [la Ha] [lb Hb]. exists (plus la lb). by apply is_series_plus. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy