proposition: Lemma is_series_minus (a b : nat -> V) (la lb : V) : is_series a la -> is_series b lb -> is_series (fun n => plus (a n) (opp (b n))) (plus la (opp lb)).
proof: Proof. move => Ha Hb. apply is_series_plus => //. apply is_series_opp => //. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy