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