proposition: Lemma Series_opp (a : nat -> R) : Series (fun n => - a n) = - Series a.
proof: Proof. rewrite /Series (Lim_seq_ext (sum_n (fun k : nat => - a k)) (fun n => - (sum_n (fun k => a k) n))). rewrite Lim_seq_opp. by rewrite Rbar_opp_real. elim => [ | n IH]. rewrite !sum_O ; ring. rewrite !sum_Sn IH /plus /=. ring. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy