proposition: Lemma PSeries_plus (a b : nat -> R) (x : R) : ex_pseries a x -> ex_pseries b x -> PSeries (PS_plus a b) x = PSeries a x + PSeries b x.
proof: Proof. intros Ha Hb. apply is_pseries_unique. apply: is_pseries_plus ; rewrite PSeries_eq ; apply Series_correct. by apply Ha. by apply Hb. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series