proposition: Lemma is_pseries_opp (a : nat -> V) (x :K) (l : V) : is_pseries a x l -> is_pseries (PS_opp a) x (opp l).
proof: Proof. intros H. replace (opp l) with (scal (opp (one : K)) l). 2: now rewrite scal_opp_l scal_one. apply is_pseries_ext with (PS_scal (opp one) a). intros n; unfold PS_scal, PS_opp. now rewrite scal_opp_l scal_one. apply is_pseries_scal. rewrite -opp_mult_l -opp_mult_r. by rewrite mult_one_l mult_one_r. by apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series