proposition: Lemma Cauchy_Lim_prop4_prop3 : forall seq y, Cauchy_Lim_prop4 seq y -> Cauchy_Lim_prop3 seq y.
proof: Proof. intros. unfold Cauchy_Lim_prop4 in H. unfold Cauchy_Lim_prop3 in |- *. intros. exists k. intros. apply AbsSmall_leEq_trans with (one_div_succ (R:=IR) m). 2: apply H. apply one_div_succ_resp_leEq. assumption. Qed.
imports: CoRN.reals.CReals Coq(Lia)