proposition: Lemma maj_by_pos : forall Un:nat -> R, { l:R | Un_cv Un l } -> exists l : R, 0 < l /\ (forall n:nat, Rabs (Un n) <= l).
proof: Proof. intros Un X; elim X; intros. cut { l:R | Un_cv (fun k:nat => Rabs (Un k)) l }. - intro X0. assert (H := CV_Cauchy (fun k:nat => Rabs (Un k)) X0). assert (H0 := cauchy_bound (fun k:nat => Rabs (Un k)) H). elim H0; intros. exists (x0 + 1). cut (0 <= x0). + intro. split. * apply Rplus_le_lt_0_compat; [ assumption | apply Rlt_0_1 ]. * intros. apply Rle_trans with x0. -- unfold is_upper_bound in H1. apply H1. exists n; reflexivity. -- pattern x0 at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; apply Rlt_0_1. + apply Rle_trans with (Rabs (Un 0%nat)). * apply Rabs_pos. * unfold is_upper_bound in H1. apply H1. exists 0%nat; reflexivity. - exists (Rabs x). apply cv_cvabs; assumption. Qed.
imports: Rbase Rfunctions Rseries Lia