proposition: Lemma Lim_wd'' : forall seq1 seq2 : CauchySeqR, {N : nat | forall n : nat, N <= n -> seq1 n [=] seq2 n} -> Lim seq1 [=] Lim seq2.
proof: Proof. intros seq1 seq2 H. destruct H as [N H]. cut (Cauchy_Lim_prop2 seq1 (Lim seq2)). intro. apply eq_symmetric_unfolded. apply Limits_unique; assumption. apply Cauchy_Lim_prop2_wd' with (seq2:nat -> IR). apply Cauchy_complete. exists N. intros; apply eq_symmetric_unfolded. auto. Qed.
imports: CoRN.reals.CReals Coq(Lia)