proposition: Lemma is_series_unique (a : nat -> R) (l : R) : is_series a l -> Series a = l.
proof: Proof. move => Ha. replace l with (real (Finite l)) by auto. apply (f_equal real). by apply is_lim_seq_unique. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy