proposition: Lemma CV_ALT_step3 : forall (Un:nat -> R) (N:nat), Un_decreasing Un -> positivity_seq Un -> sum_f_R0 (fun i:nat => tg_alt Un (S i)) N <= 0.
proof: Proof. intros; induction N as [| N HrecN]. - simpl; unfold tg_alt; simpl; rewrite Rmult_1_r. apply Rplus_le_reg_l with (Un 1%nat). rewrite Rplus_0_r; replace (Un 1%nat + -1 * Un 1%nat) with 0; [ apply H0 | ring ]. - assert (H1 := even_odd_cor N). elim H1; intros. elim H2; intro. + rewrite H3; apply CV_ALT_step2; assumption. + rewrite H3; rewrite tech5. apply Rle_trans with (sum_f_R0 (fun i:nat => tg_alt Un (S i)) (S (2 * x))). * pattern (sum_f_R0 (fun i:nat => tg_alt Un (S i)) (S (2 * x))) at 2; rewrite <- Rplus_0_r. apply Rplus_le_compat_l. unfold tg_alt; simpl. replace (x + (x + 0))%nat with (2 * x)%nat; [ idtac | ring ]. rewrite pow_1_even. replace (-1 * (-1 * (-1 * 1)) * Un (S (S (S (2 * x))))) with (- Un (S (S (S (2 * x))))); [ idtac | ring ]. apply Rplus_le_reg_l with (Un (S (S (S (2 * x))))). rewrite Rplus_0_r; rewrite Rplus_opp_r. apply H0. * apply CV_ALT_step2; assumption. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra