proposition: Lemma is_pseries_plus (a b : nat -> V) (x :K) (la lb : V) : is_pseries a x la -> is_pseries b x lb -> is_pseries (PS_plus a b) x (plus la lb).
proof: Proof. move => Ha Hb. apply filterlim_ext with (f:= (fun n => plus (sum_n (fun k => scal (pow_n x k) (a k)) n) (sum_n (fun k => scal (pow_n x k) (b k)) n))). elim => [ | n IH]. simpl ; rewrite /PS_plus !sum_O. now repeat rewrite scal_one. simpl ; rewrite !sum_Sn -IH /PS_plus. generalize (sum_n (fun k : nat => scal (pow_n x k) (a k)) n) => a' ; generalize (sum_n (fun k : nat => scal (pow_n x k) (b k)) n) => b'. repeat rewrite -plus_assoc; apply f_equal. rewrite plus_comm -plus_assoc; apply f_equal. rewrite scal_distr_l; apply plus_comm. now apply filterlim_comp_2 with (3 := filterlim_plus _ _). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series