proposition: Lemma CV_disk_DAlembert_aux (a : nat -> R) (x k : R) : x <> 0 -> (forall n, a n <> 0) -> (is_lim_seq (fun n => Rabs (a (S n) / a n)) k <-> is_lim_seq (fun n => Rabs ((a (S n) * x^(S n)) / (a n * x ^ n))) (Rabs x * k)).
proof: Proof. move => Hx Ha ; split => H. evar (l : Rbar). replace (Finite (Rabs x * k)) with l. apply is_lim_seq_ext with (fun n => Rabs x * Rabs (a (S n) / a n)). move => n ; rewrite ?Rabs_div => //=. rewrite ?Rabs_mult. field. split ; apply Rabs_no_R0 => //. by apply pow_nonzero. apply Rmult_integral_contrapositive_currified => //. by apply pow_nonzero. apply is_lim_seq_scal_l. apply H. by simpl. evar (l : Rbar). replace (Finite k) with l. apply is_lim_seq_ext with (fun n : nat => /Rabs x * Rabs (a (S n) * x ^ S n / (a n * x ^ n))). move => n ; rewrite /= ?Rabs_div ?Rabs_mult. field. repeat split ; apply Rabs_no_R0 => //. by apply pow_nonzero. by apply Ha. apply Rmult_integral_contrapositive_currified => //. by apply pow_nonzero. apply is_lim_seq_scal_l. apply H. apply Rbar_finite_eq ; field. apply Rabs_no_R0 => //. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series