proposition: Lemma lub_is_finite_cv_radius : (forall (P : Prop), P \/ ~P) -> forall (An : Rseq) (r : R), is_lub (Cv_radius_weak An) r -> finite_cv_radius An r.
proof: Proof. intros EM An r [rho_ub rho_l] ; split. intros r' [r'_pos r'_bd]. destruct (EM (Cv_radius_weak An r')) as [P | nP]. assumption. destruct (Rlt_irrefl r); apply Rle_lt_trans with r' ; [apply rho_l | assumption] ; intros b Hf ; fold (Cv_radius_weak An b) in Hf ; destruct (Rle_lt_dec b r') as [b_le_r' | r'_lt_b] ; [assumption | destruct nP] ; apply Cv_radius_weak_le_compat with b. rewrite Rabs_pos_eq ; [rewrite Rabs_pos_eq |] ; [left | left ; apply Rle_lt_trans with r' |] ; assumption. assumption. intros r' r'_lb Hf ; apply (Rlt_irrefl r) ; apply Rlt_le_trans with r' ; [| apply rho_ub] ; assumption. 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