proposition: Lemma Cauchy_Lim_prop3_prop2 : forall seq y, Cauchy_Lim_prop3 seq y -> Cauchy_Lim_prop2 seq y.
proof: Proof. intros seq y H. unfold Cauchy_Lim_prop2 in |- *. intros eps H0. unfold Cauchy_Lim_prop3 in H. generalize (pos_ap_zero _ _ H0); intro Heps. elim (Archimedes ([1][/] eps[//]Heps)). intro K; intros H1. elim (H K). intro N; intros H2. exists N. intros m H3. generalize (H2 _ H3); intro H4. apply AbsSmall_leEq_trans with (one_div_succ (R:=IR) K); try assumption. unfold one_div_succ in |- *. unfold Snring in |- *. apply shift_div_leEq'. apply nring_pos. auto with arith. apply leEq_transitive with (eps[*]nring K). apply shift_leEq_mult' with Heps; assumption. astepl (nring K[*]eps). apply less_leEq. apply mult_resp_less; try assumption. apply nring_less. auto with arith. Qed.
imports: CoRN.reals.CReals Coq(Lia)