proposition: Lemma Limits_unique : forall (seq : CauchySeq IR) y, Cauchy_Lim_prop2 seq y -> y [=] Lim seq.
proof: Proof. intros seq y H. apply not_ap_imp_eq. unfold not in |- *; intro H0. generalize (ap_imp_less _ _ _ H0); intro H1. elim H1; intro H2. elim (less_Lim_so _ _ H2); intro eps; intros H4 H5. elim H5; intro N; intro H6. unfold Cauchy_Lim_prop2 in H. elim (H _ H4); intro N'; intro H7. generalize (Nat.le_max_l N N'); intro H8. generalize (Nat.le_max_r N N'); intro H9. generalize (H6 _ H8); intro H10. generalize (H7 _ H9); intro H11. elim H11; intros H12 H13. apply (less_irreflexive_unfolded _ (y[+]eps)). eapply less_leEq_trans. apply H10. apply plus_cancel_leEq_rht with ([--]y). rstepr eps. exact H13. elim (Lim_less_so _ _ H2); intro eps; intros H4 H5. elim H5; intro N; intros H6. unfold Cauchy_Lim_prop2 in H. elim (H _ H4); intro N'; intros H7. generalize (Nat.le_max_l N N'); intro H8. generalize (Nat.le_max_r N N'); intro H9. generalize (H6 _ H8); intro H10. generalize (H7 _ H9); intro H11. elim H11; intros H12 H13. apply (less_irreflexive_unfolded _ y). eapply leEq_less_trans. 2: apply H10. apply plus_cancel_leEq_rht with ([--]y[-]eps). rstepl ([--]eps). rstepr (seq (Nat.max N N') [-]y). assumption. Qed.
imports: CoRN.reals.CReals Coq(Lia)