proposition: Lemma Alembert_C5 : forall (An:nat -> R) (k:R), 0 <= k < 1 -> (forall n:nat, An n <> 0) -> Un_cv (fun n:nat => Rabs (An (S n) / An n)) k -> { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }.
proof: Proof. intros. assert (Hyp0:{ l:R | Un_cv (fun N:nat => sum_f_R0 An N) l } -> { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }). { intro X. elim X; intros. exists x. assumption. } apply Hyp0. apply cv_cauchy_2. apply cauchy_abs. apply cv_cauchy_1. assert (Hyp:{ l:R | Un_cv (fun N:nat => sum_f_R0 (fun i:nat => Rabs (An i)) N) l } -> { l:R | Un_cv (fun N:nat => sum_f_R0 (fun i:nat => Rabs (An i)) N) l }). { intro X. elim X; intros. exists x. assumption. } apply Hyp. apply (Alembert_C4 (fun i:nat => Rabs (An i)) k). - assumption. - intro; apply Rabs_pos_lt; apply H0. - unfold Un_cv. unfold Un_cv in H1. unfold Rdiv. intros. elim (H1 eps H2); intros. exists x; intros. rewrite <- Rabs_inv. rewrite <- Rabs_mult. rewrite Rabs_Rabsolu. unfold Rdiv in H3; apply H3; assumption. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra