proposition: Lemma CV_ALT_step4 : forall Un:nat -> R, Un_decreasing Un -> positivity_seq Un -> has_ub (fun N:nat => sum_f_R0 (tg_alt Un) (S (2 * N))).
proof: Proof. intros; unfold has_ub; unfold bound. exists (Un 0%nat). unfold is_upper_bound; intros; elim H1; intros. rewrite H2; rewrite decomp_sum. - replace (tg_alt Un 0) with (Un 0%nat). + pattern (Un 0%nat) at 2; rewrite <- Rplus_0_r. apply Rplus_le_compat_l. apply CV_ALT_step3; assumption. + unfold tg_alt; simpl; ring. - apply Nat.lt_0_succ. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra