proposition: Lemma CV_radius_decr_1 (a : nat -> R) : CV_radius (PS_decr_1 a) = CV_radius a.
proof: Proof. assert (Ha := CV_radius_bounded a). assert (Ha' := CV_radius_bounded (PS_decr_1 a)). apply Rbar_le_antisym. apply Ha' => x [M Hx] ; apply Ha. eexists ; case => [ | n] ; simpl. eapply Rle_trans, Rmax_l. rewrite Rmult_1_r ; apply Rle_refl. eapply Rle_trans, Rmax_r. rewrite (Rmult_comm x) -Rmult_assoc Rabs_mult. apply Rmult_le_compat_r. by apply Rabs_pos. by apply Hx. apply Ha => x [M Hx] ; apply Ha'. move: (fun n => Hx (S n)) => {} Hx ; simpl in Hx. case: (Req_dec x 0) => Hx0. rewrite Hx0 ; exists (Rabs (a 1%nat)) ; case => /= [ | n]. rewrite Rmult_1_r ; by right. rewrite Rmult_0_l Rmult_0_r Rabs_R0. by apply Rabs_pos. exists (M / Rabs x) => n. apply Rle_div_r. by apply Rabs_pos_lt. rewrite -Rabs_mult Rmult_assoc (Rmult_comm _ x). by apply Hx. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series