proposition: Lemma CV_disk_outside (a : nat -> R) (x : R) : Rbar_lt (CV_radius a) (Finite (Rabs x)) -> ~ is_lim_seq (fun n => a n * x ^ n) 0.
proof: Proof. case: (CV_radius_bounded a) => ub lub. move => Hx. have H : ~ (fun r : R => exists M : R, forall n : nat, Rabs (a n * r ^ n) <= M) x. contradict Hx ; apply Rbar_le_not_lt. apply ub. case: Hx => M Hx. exists M => n. by rewrite Rabs_mult RPow_abs Rabs_Rabsolu -Rabs_mult. contradict H. apply is_lim_seq_spec in H. case: (H (mkposreal _ Rlt_0_1)) => /= {Hx} N Hx. set M := fix f N := match N with | O => Rabs (a O * x ^ O) | S n => Rmax (f n) (Rabs (a (n) * x ^ (n))) end. exists (Rmax (M N) 1) => n. case: (le_lt_dec N n) => Hn. apply Rle_trans with (2 := Rmax_r _ _). move: (Hx n Hn). rewrite Rminus_0_r. by apply Rlt_le. apply Rle_trans with (2 := Rmax_l _ _). elim: N n Hn {Hx} => [ | N IH] /= n Hn. by apply Nat.nlt_0_r in Hn. apply ->Nat.lt_succ_r in Hn. destruct (proj1 (Nat.le_lteq _ _) Hn) as [Hn' | ->]. - now apply Rle_trans with (2 := Rmax_l _ _), IH. - now apply Rle_trans with (2 := Rmax_r _ _), Rle_refl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series