Lemma isaprop_ex_lim_seq : ∏ u : nat -> NonnegativeReals, isaprop (∑ l : NonnegativeReals, is_lim_seq u l). 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.
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.