proposition: Lemma decreasing_cv : forall Un:nat -> R, Un_decreasing Un -> has_lb Un -> { l:R | Un_cv Un l }.
proof: Proof. intros. cut ({ l:R | Un_cv (opp_seq Un) l } -> { l:R | Un_cv Un l }). - intro X. apply X. apply growing_cv. + apply decreasing_growing; assumption. + exact H0. - intros (x,p). exists (- x). unfold Un_cv in p. unfold Rdist in p. unfold opp_seq in p. unfold Un_cv. unfold Rdist. intros. elim (p eps H1); intros. exists x0; intros. assert (H4 := H2 n H3). rewrite <- Rabs_Ropp. replace (- (Un n - - x)) with (- Un n - x); [ assumption | ring ]. Qed.
imports: Rbase Rfunctions Rseries Lia