proposition: Lemma AltSeries_small_neg_even : forall p x, Str_alt_decr x -> 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)) <= 0.
proof: Proof. assert (forall x, Str_alt_decr x -> 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)) <= 0). { intros. 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. destruct H. apply (Qplus_le_l _ _ (-q)). rewrite <- Qplus_assoc, Qplus_opp_r, Qplus_0_r. apply (Qle_trans _ _ _ (Qle_Qabs _)). apply (Qle_trans _ _ _ H). rewrite Qplus_0_l, Qabs_neg. apply Qle_refl. exact H0. } apply (Pos.peano_ind (fun p => forall x, Str_alt_decr x -> 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)) <= 0)). - intros. exact (H x H0 H1). - intros. rewrite <- (Qplus_0_r 0). 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). simpl. pose proof (Str_alt_even_step 1 x H1). unfold Str_pth in H3. simpl in H3. apply Qnot_lt_le. intro abs. rewrite <- (Qmult_0_l (snd (f (f (f x))))) in H3. apply Qmult_le_r in H3. 2: exact abs. apply (Qle_antisym _ _ H2) in H3. clear H2. apply (Str_alt_zero 1 _ H1) in H3. apply (Str_alt_zero 2 _ H1) in H3. unfold Str_pth in H3. simpl in H3. rewrite H3 in abs. exact (Qlt_irrefl 0 abs). 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