proposition: Lemma is_lim_seq_unique (u : nat → NonnegativeReals) (l l' : NonnegativeReals) : is_lim_seq u l → is_lim_seq u l' → l = l'.
proof: Proof. intros Hl Hl'. apply istight_apNonnegativeReals. unfold neg ; apply sumofmaps. - now apply (is_lim_seq_unique_aux u). - now apply (is_lim_seq_unique_aux u). Qed.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.RealNumbers.Sets UniMath.Algebra.ConstructiveStructures UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.NonnegativeRationals