proposition: Lemma AltSeries_further : forall x (p q : positive) (d1 d2 ε1 ε2 : Qpos), Str_alt_decr x -> Qabs (Str_pth p x) <= proj1_sig ε1 -> Qabs (Str_pth q x) <= proj1_sig ε2 -> proj1_sig d1 <= proj1_sig ε1 -> proj1_sig d2 <= proj1_sig ε2 -> Qball (proj1_sig ε1 + proj1_sig ε2) (SumStream x p d1) (SumStream x q d2).
proof: Proof. intros. unfold SumStream. pose proof (iterate_stop_correct _ (fun y : X * Q * Q => let (z, r) := f (fst y) in (z, r, Qred (r + snd y))) (fun y : X * Q * Q => Qle_bool (Qabs (snd (fst y))) (` d1)) p (x,0)) as [r [req [_ H4]]]. rewrite req. clear req. assert (Qabs (Str_pth r x) <= proj1_sig ε1) as rstop. { destruct H4. rewrite <- H4. exact H0. destruct H4. rewrite SumStream_fst_red in H5. unfold fst in H5. apply Qle_bool_iff in H5. exact (Qle_trans _ _ _ H5 H2). } clear H4 H2 d1 H0 p. rewrite SumStream_red. pose proof (iterate_stop_correct _ (fun y : X * Q * Q => let (z, r) := f (fst y) in (z, r, Qred (r + snd y))) (fun y : X * Q * Q => Qle_bool (Qabs (snd (fst y))) (` d2)) q (x,0)) as [s [seq [_ H2]]]. rewrite seq. clear seq. assert (Qabs (Str_pth s x) <= proj1_sig ε2) as sstop. { destruct H2. rewrite <- H0. exact H1. destruct H0. rewrite SumStream_fst_red in H2. unfold fst in H2. apply Qle_bool_iff in H2. exact (Qle_trans _ _ _ H2 H3). } clear H2 H3 d2 H1 q. rewrite SumStream_red. destruct (Pos.lt_total r s). - unfold Qball. rewrite <- (Pplus_minus s r). 2: apply Pos.lt_gt, H0. apply AbsSmall_Qabs. rewrite (SumStream_assoc x r (s-r)). unfold Qminus. assert (forall a b : Q, -(a+b) == -a+-b). { intros. ring. } rewrite H1, Qplus_assoc, Qplus_opp_r, Qplus_0_l. clear H1. rewrite Qabs_opp. refine (Qle_trans _ _ _ (AltSeries_small _ _ _) _). apply Str_alt_decr_tl, H. rewrite <- iterate_succ. destruct (H r). apply (Qle_trans _ _ _ H1). apply (Qle_trans _ (` ε1 + 0)). rewrite Qplus_0_r. exact rstop. apply Qplus_le_r, Qpos_nonneg. - destruct H0. rewrite H0. apply ball_refl, (Qpos_nonneg (ε1 + ε2)). unfold Qball. rewrite <- (Pplus_minus r s). 2: apply Pos.lt_gt, H0. apply AbsSmall_Qabs. rewrite (SumStream_assoc x s (r-s)). rewrite Qplus_comm. unfold Qminus. rewrite <- Qplus_assoc, Qplus_opp_r, Qplus_0_r. refine (Qle_trans _ _ _ (AltSeries_small _ _ _) _). apply Str_alt_decr_tl, H. rewrite <- iterate_succ. destruct (H s). apply (Qle_trans _ _ _ H1). apply (Qle_trans _ (0 + ` ε2)). rewrite Qplus_0_l. exact sstop. apply Qplus_le_l, Qpos_nonneg. 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