proposition: Lemma CV_radius_const_0 : CV_radius (fun _ => 0) = p_infty.
proof: Proof. suff : forall x, Rbar_le (Rabs x) (CV_radius (fun _ : nat => 0)). case H : (CV_radius (fun _ : nat => 0)) => [cv | | ] //= H0. case: (Rle_lt_dec 0 cv) => Hcv. move: (H0 (cv + 1)) => {} H0. contradict H0 ; apply Rlt_not_le => /=. apply Rlt_le_trans with (2 := Rle_abs _). apply Rminus_lt_0 ; ring_simplify ; by apply Rlt_0_1. contradict Hcv ; apply (Rbar_le_not_lt cv 0). rewrite -Rabs_R0. by apply H0. move: (H0 0) => {} H0. contradict H0 ; by apply Rbar_lt_not_le. move => x ; apply Rbar_not_lt_le => Hx. apply CV_disk_outside in Hx. apply: Hx. apply is_lim_seq_ext with (fun _ => 0). move => n ; ring. by apply is_lim_seq_const. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series