proposition: Lemma Lim_CauchySeq2 : forall seq y H, Lim (Build_CauchySeq2_y seq y H) [=] y.
proof: Proof. intros. apply eq_symmetric_unfolded. apply Limits_unique. unfold Build_CauchySeq2_y in |- *. unfold Build_CauchySeq2 in |- *. unfold CS_seq in |- *. assumption. Qed.
imports: CoRN.reals.CReals Coq(Lia)