proposition: Lemma CV_disk_DAlembert (a : nat -> R) (x:R) l : (forall n:nat, a n <> 0) -> is_lim_seq (fun n:nat => Rabs (a (S n) / a n)) (Finite l) -> (l = 0 \/ (l <> 0 /\ Rabs x < / l)) -> CV_disk a x.
proof: Proof. move => Ha Hl H. case: (Req_dec x 0) => Hx. rewrite Hx. exists (Rabs (a O)). apply (is_lim_seq_ext (fun _ => Rabs (a O)) _ (Rabs (a 0%nat))). elim => /= [ | n IH]. by rewrite sum_O Rmult_1_r. by rewrite sum_Sn /= Rmult_0_l Rmult_0_r Rabs_R0 /plus /= Rplus_0_r. apply is_lim_seq_const. apply ex_series_DAlembert with (Rabs x * l). case: H => H. rewrite H Rmult_0_r ; by apply Rlt_0_1. replace 1 with (/ l * l) by (field ; apply H). apply Rmult_lt_compat_r. apply Rnot_le_lt ; case => H0. case: H => H. apply Rle_not_lt. apply Rlt_le, Rlt_le_trans with 0. by apply Rinv_lt_0_compat. by apply Rabs_pos. by case: H. by apply H. move => n ; apply Rmult_integral_contrapositive_currified. by apply Ha. by apply pow_nonzero. by apply CV_disk_DAlembert_aux. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series