proposition: Lemma is_series_opp (a : nat -> V) (la : V) : is_series a la -> is_series (fun n => opp (a n)) (opp la).
proof: Proof. move => Ha. apply filterlim_ext with (fun n => opp (sum_n a n)). elim => [ | n IH]. rewrite !sum_O ; easy. rewrite !sum_Sn -IH. apply: opp_plus. apply filterlim_comp with (1:=Ha). apply filterlim_opp. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy