Lemma is_lim_seq_unique (u : nat → NonnegativeReals) (l l' : NonnegativeReals) : is_lim_seq u l → is_lim_seq u l' → l = l'. 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.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals.