proposition: Lemma finite_cv_radius_is_lub : forall (An : Rseq) (r : R), finite_cv_radius An r -> is_lub (Cv_radius_weak An) r.
proof: Proof. intros An r [rho rho_ub] ; split. intros r' Hr' ; destruct (Rle_lt_dec r' r) as [r'ler | rltr']. assumption. destruct (rho_ub _ rltr' Hr'). intros r' Hr' ; destruct (Rle_lt_dec r r') as [rler' | r'ltr]. assumption. assert (H : has_ub (gt_abs_pser An (middle r' r))). assert (r'_pos : 0 <= r'). apply Hr' ; apply Cv_radius_weak_0. apply rho ; split ; [apply middle_le_le_pos ; [| left ; apply Rle_lt_trans with r'] | apply middle_is_in_the_middle] ; assumption. assert (Hf := Hr' _ H). assert (Hf' : r' < middle r' r) by (apply middle_is_in_the_middle ; assumption). clear -Hf Hf' ; apply False_ind ; lra. Qed.
imports: Reals Rpser_def Rpser_def_simpl Rinterval Rsequence_def Rsequence_base_facts Rsequence_subsequence Rsequence_rewrite_facts Rsequence_cv_facts Rsequence_facts Rsequence_bound_facts Rsequence_sums_facts Rpow_facts PeanoNat Lra MyRIneq MyNat MyNNR