proposition: Lemma cv_cvabs : forall (Un:nat -> R) (l:R), Un_cv Un l -> Un_cv (fun i:nat => Rabs (Un i)) (Rabs l).
proof: Proof. unfold Un_cv; unfold Rdist; intros. elim (H eps H0); intros. exists x; intros. apply Rle_lt_trans with (Rabs (Un n - l)). - apply Rabs_triang_inv2. - apply H1; assumption. Qed.
imports: Rbase Rfunctions Rseries Lia