proposition: Lemma Cauchy_Lim_prop4_prop2 : forall seq y, Cauchy_Lim_prop4 seq y -> Cauchy_Lim_prop2 seq y.
proof: Proof. intros. apply Cauchy_Lim_prop3_prop2. apply Cauchy_Lim_prop4_prop3. assumption. Qed.
imports: CoRN.reals.CReals Coq(Lia)