proposition: Lemma Series_ext (a b : nat -> R) : (forall n, a n = b n) -> Series a = Series b.
proof: Proof. move => Heq. apply (f_equal real). apply Lim_seq_ext. intros n; now apply sum_n_m_ext. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy