proposition: Lemma AltSeries_small_pos : forall x (p : positive), 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 (x, 0)) <= snd (f x).
proof: Proof. intros x p. revert p x. 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 (x, 0)) <= snd (f x))). - intros. simpl. destruct (f x). simpl. rewrite Qplus_0_r. split. exact H0. apply Qle_refl. - intros. destruct p. + split. rewrite Pos.xI_succ_xO, <- Pos.double_succ. exact (AltSeries_small_pos_even _ x H0 H1). rewrite <- Pos.add_1_r. rewrite SumStream_assoc, iterate_one. specialize (H x H0 H1) as [_ H]. apply (Qle_trans _ (snd (CRstreams.iterate _ (fun y : X * Q * Q => let (z, r0) := f (fst y) in (z, r0, r0 + snd y)) p~1 (x, 0)) + 0)). 2: rewrite Qplus_0_r; exact H. apply Qplus_le_r. unfold fst. apply (Qle_trans _ (snd (f (CRstreams.iterate (X * Q) f p~1 x)))). destruct (f (CRstreams.iterate (X * Q) f p~1 x)). simpl. rewrite Qplus_0_r. apply Qle_refl. rewrite <- iterate_succ. pose proof (Str_alt_neg (Pos.succ p) x H0 H1). specialize (H0 (p~1)%positive) as [_ H0]. unfold Str_pth in H0. exact H2. + split. rewrite <- Pos.add_1_r. rewrite SumStream_assoc, iterate_one. rewrite <- (Qplus_0_r 0). apply Qplus_le_compat. exact (AltSeries_small_pos_even _ x H0 H1). apply (Qle_trans _ (snd (f (CRstreams.iterate (X * Q) f p~0 x)))). rewrite <- iterate_succ, <- Pos.xI_succ_xO. exact (Str_alt_pos _ x H0 H1). unfold fst. destruct (f (CRstreams.iterate (X * Q) f p~0 x)). simpl. rewrite Qplus_0_r. apply Qle_refl. rewrite <- Pos.add_1_l, SumStream_assoc, iterate_one. simpl (fst (x,0)). rewrite <- (Qplus_0_r (snd (f x))). setoid_replace (snd (let (z, r0) := f x in (z, r0, r0 + snd (x, 0)))) with (snd (f x)) by (destruct (f x); apply Qplus_0_r). apply Qplus_le_r. apply AltSeries_small_neg_even. apply (Str_alt_decr_tl x _ H0). rewrite <- iterate_succ. apply (Str_alt_neg _ x H0 H1). + pose proof (Str_alt_neg 1 x H0 H1) as sndNeg. unfold Str_pth in sndNeg. simpl in sndNeg. specialize (H0 xH). unfold Str_pth in H0. simpl in H0. simpl. destruct (f x). simpl. simpl in H0. unfold snd in H1. destruct (f (x0,q)). simpl. simpl in H0. rewrite Qplus_0_r. destruct H0. rewrite (Qabs_pos q) in H0. 2: exact H1. unfold snd in sndNeg. split. rewrite Qabs_neg in H0. 2: exact sndNeg. rewrite Qle_minus_iff, Qopp_involutive, Qplus_comm in H0. exact H0. apply (Qle_trans _ (0 + q)). apply Qplus_le_l. exact sndNeg. rewrite Qplus_0_l. apply Qle_refl. 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