proposition: Lemma CV_ALT_step0 : forall Un:nat -> R, Un_decreasing Un -> Un_growing (fun N:nat => sum_f_R0 (tg_alt Un) (S (2 * N))).
proof: Proof. intros; unfold Un_growing; intro. cut ((2 * S n)%nat = S (S (2 * n))). - intro; rewrite H0. do 4 rewrite tech5; repeat rewrite Rplus_assoc; apply Rplus_le_compat_l. pattern (tg_alt Un (S (2 * n))) at 1; rewrite <- Rplus_0_r. apply Rplus_le_compat_l. unfold tg_alt; rewrite <- H0; rewrite pow_1_odd; rewrite pow_1_even; rewrite Rmult_1_l. apply Rplus_le_reg_l with (Un (S (2 * S n))). rewrite Rplus_0_r; replace (Un (S (2 * S n)) + (Un (2 * S n)%nat + -1 * Un (S (2 * S n)))) with (Un (2 * S n)%nat); [ idtac | ring ]. apply H. - cut (forall n:nat, S n = (n + 1)%nat); [ intro | intro; ring ]. rewrite (H0 n); rewrite (H0 (S (2 * n))); rewrite (H0 (2 * n)%nat); ring. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra