proposition: Lemma is_pseries_Reals (a : nat -> R) (x l : R) : is_pseries a x l <-> Pser a x l.
proof: Proof. split => H. move => e He ; set eps := mkposreal e He. apply (is_lim_seq_spec _ l) in H. case: (H eps) => {H} N H. exists N => n Hn. rewrite <- sum_n_Reals. rewrite (sum_n_ext _ (fun n0 : nat => scal (pow_n x n0) (a n0))). by apply H. intros k; rewrite pow_n_pow /=; apply Rmult_comm. apply (is_lim_seq_spec _ l). move => eps. case: (H eps (cond_pos eps)) => {H} N H. exists N => n Hn. rewrite (sum_n_ext _ (fun n0 : nat => a n0 * x ^ n0)). rewrite sum_n_Reals. by apply H. intros; now rewrite Rmult_comm pow_n_pow. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series