proposition: Theorem alternated_series : forall Un:nat -> R, Un_decreasing Un -> Un_cv Un 0 -> { l:R | Un_cv (fun N:nat => sum_f_R0 (tg_alt Un) N) l }.
proof: Proof. intros; apply CV_ALT. - assumption. - unfold positivity_seq; apply decreasing_ineq; assumption. - assumption. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra