proposition: Lemma AltSeries_small_pos_even : forall p x, Str_alt_decr x -> 0 <= snd (f x) -> 0 <= snd (CRstreams.iterate (X * Q * Q) (fun y : X * Q * Q => let (z, r0) := f (fst y) in (z, r0, r0 + snd y)) (p~0) (x, 0)).
proof: Proof. assert (forall x, Str_alt_decr x -> 0 <= snd (f x) -> 0 <= snd (CRstreams.iterate (X * Q * Q) (fun y : X * Q * Q => let (z, r0) := f (fst y) in (z, r0, r0 + snd y)) (1 + 1) (x, 0))). { intros. pose proof (Str_alt_neg 1 x H H0) as H1. unfold Str_pth in H1. simpl in H1. specialize (H xH). simpl. unfold Str_pth in H. simpl in H. destruct (f x); simpl. simpl in H. unfold snd in H0. destruct (f (x0,q)); simpl. rewrite Qplus_0_r. simpl in H. unfold snd in H1. destruct H. rewrite Qabs_neg in H. 2: exact H1. rewrite Qabs_pos in H. 2: exact H0. apply Qle_minus_iff in H. rewrite Qopp_involutive, Qplus_comm in H. exact H. } apply (Pos.peano_ind (fun p => forall x, Str_alt_decr x -> 0 <= snd (f x) -> 0 <= snd (CRstreams.iterate (X * Q * Q) (fun y : X * Q * Q => let (z, r0) := f (fst y) in (z, r0, r0 + snd y)) (p~0) (x, 0)))). - intros. exact (H x H0 H1). - intros. rewrite <- Qplus_0_r. rewrite Pos.double_succ, <- Pos.add_1_l, <- Pos.add_1_l. rewrite Pos.add_assoc, SumStream_assoc. apply Qplus_le_compat. exact (H x H1 H2). apply H0. exact (Str_alt_decr_tl x 2 H1). rewrite <- iterate_succ. exact (Str_alt_pos _ x H1 H2). Qed.
imports: Coq.setoid_ring.ArithRing Coq.Bool.Bool Coq.QArith.Qpower Coq.QArith.Qabs CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.model.metric2.Qmetric CoRN.reals.fast.LazyNat CoRN.reals.fast.CRstreams CoRN.metric2.Limit CoRN.model.totalorder.QposMinMax CoRN.classes.Qclasses MathClasses.interfaces.abstract_algebra