proposition: Lemma PSeries_opp (a : nat -> R) (x : R) : PSeries (PS_opp a) x = - PSeries a x.
proof: Proof. replace (- PSeries a x) with ((-1) * PSeries a x) by ring. rewrite -PSeries_scal. apply PSeries_ext => n. by rewrite /PS_scal /PS_opp scal_opp_one. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series