proposition: Lemma Rseq_cv_unique : forall Un lu1 lu2, Rseq_cv Un lu1 -> Rseq_cv Un lu2 -> lu1 = lu2.
proof: Proof. intros Un lu1 lu2 H1 H2. assert (H: forall eps, eps > 0 -> Rabs (lu1 - lu2) <= eps). intros eps Heps. destruct (H1 (eps / 2)%R) as [N1 HN1]; [lra|]. destruct (H2 (eps / 2)%R) as [N2 HN2]; [lra|]. pose (N := Nat.max N1 N2). replace (lu1 - lu2)%R with ((lu1 - Un N) + (Un N - lu2))%R by field. replace eps with (eps / 2 + eps / 2)%R by field. eapply Rle_trans; [apply Rabs_triang|]. apply Rplus_le_compat. left; rewrite Rabs_minus_sym; apply HN1; apply Nat.le_max_l. left; apply HN2; apply Nat.le_max_r. apply Rle_antisym; apply le_epsilon; intros eps Heps; apply H in Heps; unfold Rabs in Heps; destruct Rcase_abs; lra. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra