proposition: Lemma ex_pseries_odd_even (a : nat -> R) (x : R) : ex_pseries (fun n => a (2*n)%nat) (x^2) -> ex_pseries (fun n => a (2*n+1)%nat) (x^2) -> ex_pseries a x.
proof: Proof. move => [l1 H1] [l2 H2]. exists (l1 + x * l2). by apply is_pseries_odd_even. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series