proposition: Lemma isaprop_ex_lim_seq : ∏ u : nat -> NonnegativeReals, isaprop (∑ l : NonnegativeReals, is_lim_seq u l).
proof: Proof. intros u l l'. apply (iscontrweqf (X := (pr1 l = pr1 l'))). - now apply invweq, total2_paths_hProp_equiv. - rewrite (is_lim_seq_unique _ _ _ (pr2 l) (pr2 l')). apply iscontrloopsifisaset. apply pr2. 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