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