proposition: Lemma not_ex_series_DAlembert (a : nat -> R) (l : R) : l > 1 -> (forall n, a n <> 0) -> is_lim_seq (fun n => Rabs (a (S n) / a n)) l -> ~ is_lim_seq a 0.
proof: Proof. move => Hl Ha Hda Ha0. set k := (l+1)/2. have Hk1 : 1 < k. unfold k ; lra. have : exists N, forall n, (N <= n)%nat -> k <= Rabs (a (S n) / a n). apply is_lim_seq_spec in Hda. case: (fun H => Hda (mkposreal ((l-1)/2) H)) => [ | /= {Hda} H N Hda]. apply Rdiv_lt_0_compat. by apply -> Rminus_lt_0. by apply Rlt_R0_R2. exists N => n Hn. move: (Hda n Hn) => {} Hda. apply Rabs_lt_between' in Hda. replace (k) with (l - (l - 1) / 2) by (unfold k ; field). by apply Rlt_le, Hda. case => N H. apply is_lim_seq_abs_0, (is_lim_seq_incr_n _ N) in Ha0. have : forall n, Rabs (a N) * k ^ n <= Rabs (a (n + N)%nat). elim => /= [ | n IH]. rewrite Rmult_1_r ; by apply Rle_refl. replace (Rabs (a (S (n + N)))) with (Rabs (a (S (n+N)) / a (n+N)%nat) * Rabs (a (n+N)%nat)) by (rewrite -Rabs_mult ; apply f_equal ; by field). replace (Rabs (a N) * (k * k ^ n)) with (k * (Rabs (a N) * k ^ n)) by ring. apply Rmult_le_compat. by apply Rlt_le, Rlt_trans with (1 := Rlt_0_1). apply Rmult_le_pos. by apply Rabs_pos. apply pow_le. by apply Rlt_le, Rlt_trans with (1 := Rlt_0_1). by apply H, MyNat.le_add_l. by apply IH. move => {} H. have : Finite 0 = p_infty. rewrite -(Lim_seq_geom_p k Hk1). apply sym_equal. apply is_lim_seq_unique. apply is_lim_seq_ext with (fun n => / Rabs (a N) * (Rabs (a N) * k ^ n)). move => n ; field ; by apply Rabs_no_R0. rewrite -(Rmult_0_r (/Rabs (a N))). apply (is_lim_seq_scal_l _ _ (Finite 0)). apply is_lim_seq_le_le with (fun _ => 0) (fun n => Rabs (a (n + N)%nat)). move => n ; split. apply Rmult_le_pos. by apply Rabs_pos. apply pow_le. by apply Rlt_le, Rlt_trans with (1 := Rlt_0_1). by apply H. by apply is_lim_seq_const. by apply Ha0. by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy