proposition: Lemma ex_series_ext (a b : nat -> V) : (forall n, a n = b n) -> ex_series a -> ex_series b.
proof: Proof. move => Heq [l Ha]. exists l ; by apply is_series_ext with a. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy