proposition: Lemma CV_Cauchy : forall Un:nat -> R, { l:R | Un_cv Un l } -> Cauchy_crit Un.
proof: Proof. intros Un X; elim X; intros. unfold Cauchy_crit; intros. unfold Un_cv in p; unfold Rdist in p. cut (0 < eps / 2); [ intro | unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. elim (p (eps / 2) H0); intros. exists x0; intros. unfold Rdist; apply Rle_lt_trans with (Rabs (Un n - x) + Rabs (x - Un m)). - replace (Un n - Un m) with (Un n - x + (x - Un m)); [ apply Rabs_triang | ring ]. - rewrite <-(Rplus_half_diag eps); apply Rplus_lt_compat. + apply H1; assumption. + rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H1; assumption. Qed.
imports: Rbase Rfunctions Rseries Lia