proposition: Lemma ex_pseries_R (a : nat -> R) (x : R) : ex_pseries a x <-> ex_series (fun n : nat => a n * x ^ n).
proof: Proof. split ; apply ex_series_ext ; intros n ; rewrite pow_n_pow /= ; apply Rmult_comm. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series