proposition: Lemma ex_series_minus (a b : nat -> V) : ex_series a -> ex_series b -> ex_series (fun n => plus (a n) (opp (b n))).
proof: Proof. move => Ha Hb. apply ex_series_plus => //. apply ex_series_opp => //. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy