proposition: Lemma Cauchy_Lim_inv : forall seq y, Cauchy_Lim_prop2 seq y -> Cauchy_Lim_prop2 (fun n => [--] (seq n)) [--]y.
proof: Proof. intros seq y H. unfold Cauchy_Lim_prop2 in |- *. intros eps H0. elim (H _ H0); intros x H1. exists x. intros. rstepr ([--] (seq m[-]y)). apply inv_resp_AbsSmall. apply H1. assumption. Qed.
imports: CoRN.reals.CReals Coq(Lia)