proposition: Lemma Rpser_alembert_prelim2 : forall (An : nat -> R) (M : R), 0 < M -> (forall n : nat, An n <> 0) -> Rseq_eventually (fun Un => Rseq_bound Un M) (fun n => (An (S n) / An n)) -> forall r, Rabs r < / M -> Cv_radius_weak An r.
proof: Proof. intros An M M_pos An_neq An_frac_event r r_bd. destruct An_frac_event as [N HN]. assert (Rho : Cv_radius_weak (Rseq_shifts An N) r). apply Rpser_alembert_prelim with M. assumption. intro n ; apply An_neq. intro n ; unfold Rseq_shifts ; replace (N + S n)%nat with (S (N + n)) by intuition ; apply HN. assumption. rewrite Cv_radius_weak_shifts_compat. destruct Rho as [T HT] ; exists T ; intros u Hu ; destruct Hu as [n Hn] ; rewrite Hn ; apply HT ; exists n ; reflexivity. Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rsequence_facts Rsequence_sums_facts Rsequence_rewrite_facts Rpow_facts Lra PeanoNat MyRIneq MyNeq Rinterval RFsequence RFsequence_facts Tactics