proposition: Lemma alternated_series_ineq' : forall u l, Un_decreasing u -> Un_cv u 0 -> Un_cv (fun n => sum_f_R0 (tg_alt u) n) l -> forall n, (0 <= (-1)^(S n) * (l - sum_f_R0 (tg_alt u) n) <= u (S n))%R.
proof: Proof. intros u l Du Cu Cl n. destruct (even_or_odd n) as [p [Hp|Hp]]. - destruct (alternated_series_ineq u l p Du Cu Cl) as [H1 H2]. rewrite Hp, pow_1_odd. split. + lra. + apply Rplus_le_reg_r with (- sum_f_R0 (tg_alt u) (2 * p))%R. ring_simplify. replace (- sum_f_R0 (tg_alt u) (2 * p) + u (S (2 * p)))%R with (- (sum_f_R0 (tg_alt u) (2 * p) + (-1) * u (S (2 * p))))%R by ring. rewrite <- (pow_1_odd p). now apply Ropp_le_contravar. - assert (H0: S (S (2 * p)) = 2 * (p + 1)) by ring. rewrite Hp. rewrite H0 at 1 2. rewrite pow_1_even, Rmult_1_l. split. + apply Rle_0_minus. now apply alternated_series_ineq. + apply Rplus_le_reg_l with (sum_f_R0 (tg_alt u) (S (2 * p))). ring_simplify. rewrite <- (Rmult_1_l (u (S (S (2 * p))))). rewrite <- (pow_1_even (p + 1)). rewrite <- H0. destruct (alternated_series_ineq u l (p + 1) Du Cu Cl) as [_ H1]. now rewrite <- H0 in H1. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)