proposition: Lemma series_seq_Lim' : convergent -> forall H, Lim (Build_CauchySeq _ x H) [=] [0].
proof: Proof. intros. apply eq_symmetric_unfolded; apply Limits_unique. apply series_seq_Lim; auto. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)