proposition: Lemma is_series_ext (a b : nat -> V) (l : V) : (forall n, a n = b n) -> (is_series a l) -> is_series b l.
proof: Proof. move => Heq. apply filterlim_ext. intros x; now apply sum_n_m_ext. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy