Lemma is_lim_seq_unique_aux (u : nat → NonnegativeReals) (l l' : NonnegativeReals) : is_lim_seq u l → is_lim_seq u l' → l < l' → empty. Proof. intros Hl Hl' Hlt. assert (Hlt0 : 0 < l' - l). { now apply ispositive_minusNonnegativeReals. } assert (Hlt0' : 0 < (l' - l) / 2). { now apply ispositive_Dcuts_half. } generalize (Hl _ Hlt0') (Hl' _ Hlt0') ; clear Hl Hl'. apply (hinhuniv2 (P := make_hProp _ isapropempty)). intros N M. generalize (pr2 N (max (pr1 N) (pr1 M)) (max_le_l _ _)) ; intros Hn. generalize (pr2 M (max (pr1 N) (pr1 M)) (max_le_r _ _)) ; intros Hm. apply (isirrefl_Dcuts_lt_rel ((l + l') / 2)). apply istrans_Dcuts_lt_rel with (u (max (pr1 N) (pr1 M))). - apply_pr2 (plusNonnegativeReals_ltcompat_l ((l' - l) / 2)). rewrite <- isdistr_Dcuts_half_plus. rewrite (iscomm_plusNonnegativeReals l), isassoc_plusNonnegativeReals, (iscomm_plusNonnegativeReals l). rewrite <- (minusNonnegativeReals_plus_r (l' - l) l' l), isdistr_Dcuts_half_plus, <- Dcuts_half_double. + exact (pr2 Hm). + now apply Dcuts_lt_le_rel. + reflexivity. - pattern l' at 1; rewrite (minusNonnegativeReals_plus_r (l' - l) l' l), (iscomm_plusNonnegativeReals _ l), <- isassoc_plusNonnegativeReals, !isdistr_Dcuts_half_plus, <- Dcuts_half_double. + exact (pr1 Hn). + now apply Dcuts_lt_le_rel. + reflexivity. 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.