proposition: Lemma alt_bounding : forall u : nat -> R, Un_decreasing u -> (forall n, 0 <= u n) -> forall n, 0 <= sum_f_R0 (tg_alt u) n <= u O.
proof: Proof. intros Un dec pos n. pose (sum_f_R0 (tg_alt Un)) as Sn; fold Sn. assert (Heu : forall p, Sn (2 * p)%nat <= Un O). induction p. compute; intuition. eapply Rle_trans. apply CV_ALT_step1; assumption. assumption. assert (Ho0 : forall p, 0 <= Sn (S (2 * p))). induction p. unfold Sn; simpl; unfold tg_alt, pow; ring_simplify. assert (Un 1%nat <= Un O) by auto; lra. eapply Rle_trans. apply IHp. apply CV_ALT_step0; assumption. destruct (even_odd_cor n) as [p [he|ho]]; subst; split. destruct p. unfold Sn; simpl; unfold tg_alt, pow; ring_simplify; apply pos. replace (2 * S p)%nat with (S (S (2 * p))) by lia. unfold Sn; rewrite tech5; fold Sn. apply Rplus_le_le_0_compat. apply Ho0. replace (S (S (2 * p))) with (2 * S p)%nat by lia. unfold tg_alt. rewrite pow_1_even. rewrite Rmult_1_l. apply pos. apply Heu. apply Ho0. unfold Sn; rewrite tech5; fold Sn. unfold tg_alt. rewrite pow_1_odd. assert (AP : forall a b c, a <= c -> 0 <= b -> a + -1 * b <= c) by (intros; lra); apply AP; clear AP. apply Heu. apply pos. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith