proposition: Lemma ex_pseries_ext (a b : nat -> V) (x : K) : (forall n, a n = b n) -> ex_pseries a x -> ex_pseries b x.
proof: Proof. move => Heq [l Ha]. exists l ; by apply is_pseries_ext with a. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series