proposition: Lemma ex_pseries_1 (a : nat -> R) : ex_pseries a 1 <-> ex_series a.
proof: Proof. assert (forall n : nat, scal (pow_n 1 n) (a n) = a n). now intros n ; rewrite pow_n_pow pow1 scal_one. split ; apply ex_series_ext => n ; by rewrite H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series