proposition: Lemma CV_radius_plus (a b : nat -> R) : Rbar_le (Rbar_min (CV_radius a) (CV_radius b)) (CV_radius (PS_plus a b)).
proof: Proof. wlog: a b / (Rbar_le (CV_radius a) (CV_radius b)) => [ Hw | Hle ]. case: (Rbar_le_lt_dec (CV_radius a) (CV_radius b)) => Hle. by apply Hw. rewrite Rbar_min_comm. rewrite (CV_radius_ext (PS_plus a b) (PS_plus b a)). by apply Hw, Rbar_lt_le. now intros n ; apply Rplus_comm. replace (Rbar_min (CV_radius a) (CV_radius b)) with (CV_radius a). apply is_lub_Rbar_subset with (CV_disk (PS_plus a b)) (fun x => (CV_disk a x) /\ (CV_disk b x)). move => x [Ha Hb] ; by apply CV_disk_plus. rewrite /CV_radius /Lub_Rbar ; by case: ex_lub_Rbar. have Ha : is_lub_Rbar (fun x : R => CV_disk a x) (CV_radius a). rewrite /CV_radius /Lub_Rbar ; by case: ex_lub_Rbar. have Hb : is_lub_Rbar (fun x : R => CV_disk b x) (CV_radius b). rewrite /CV_radius /Lub_Rbar ; by case: ex_lub_Rbar. split. intros y [Hay Hby]. by apply Ha. case: (Rbar_le_lt_or_eq_dec _ _ (CV_radius_ge_0 a)) => Ha0. intros c Hc. assert (Rbar_le 0 c). apply Hc. split ; by apply CV_disk_0. case: c Hc H => [c | | ] //= Hc H. 2: by case: (CV_radius a). apply Rbar_not_lt_le => Hac. move: (Rbar_lt_le_trans _ _ _ Hac Hle) => Hbc. eapply Rbar_le_not_lt. apply (Hc ((c + Rbar_min (c + 1) (CV_radius a)) / 2)). assert (Rbar_lt (Rabs ((c + Rbar_min (c + 1) (CV_radius a)) / 2)) (CV_radius a)). case: (CV_radius a) Hac => //= l Hl. rewrite Rabs_pos_eq. apply Rlt_div_l. by apply Rlt_0_2. replace (l * 2) with (l+l) by ring. apply Rplus_lt_le_compat => //. by apply Rmin_r. apply Rdiv_le_0_compat. apply Rplus_le_le_0_compat => //. apply Rmin_case. apply Rplus_le_le_0_compat => //. by apply Rle_0_1. now eapply Rle_trans, Rlt_le, Hl. by apply Rlt_0_2. split ; apply CV_disk_inside. by []. now eapply Rbar_lt_le_trans, Hle. case: (CV_radius a) Hac => [l | | ] //= Hl. apply Rmin_case. apply Rlt_div_r. by apply Rlt_0_2. apply Rminus_lt_0 ; simpl ; ring_simplify. by apply Rlt_0_1. apply Rlt_div_r. by apply Rlt_0_2. apply Rminus_lt_0 ; simpl ; ring_simplify. by rewrite Rplus_comm -Rminus_lt_0. apply Rlt_div_r. by apply Rlt_0_2. apply Rminus_lt_0 ; simpl ; ring_simplify. by apply Rlt_0_1. rewrite -Ha0 in Ha Hle |- *. intros c Hc. apply Hc ; split ; by apply CV_disk_0. apply Rbar_min_case_strong => //. by apply Rbar_le_antisym. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series