proposition: Lemma AltSeries_shift : forall x cvmod decr lz, (AltSeries x cvmod decr lz == '(snd (f x)) + AltSeries (f x) _ (Str_alt_decr_tl x 1 decr) (Limit_zero_tl x cvmod 1 decr lz))%CR.
proof: Proof. intros. rewrite -> CRplus_translate. apply regFunEq_equiv, regFunEq_e. intros e. simpl. rewrite <- Pos.pred_sub. destruct (Qlt_le_dec (proj1_sig e) (Qabs (snd (f x)))). - rewrite SumStream_shift. 2: exact q. specialize (lz e). revert lz. generalize (cvmod e). apply (Pos.peano_case (fun p => Qabs (Str_pth p x) <= ` e → Qball (` e + ` e) (SumStream x p e) (SumStream x (Pos.succ (Pos.pred p)) e))). + intros. exfalso. unfold Str_pth in H. simpl in H. exact (Qlt_not_le _ _ q H). + intros. rewrite Pos.pred_succ. apply ball_refl. apply (Qpos_nonneg (e+e)). - unfold SumStream. rewrite (iterate_stop_indep _ _ _ (cvmod e) 1). rewrite (iterate_stop_indep _ _ _ (Pos.pred (cvmod e)) 1). + rewrite iterate_stop_one, iterate_stop_one. unfold fst. setoid_replace (snd (let (z, r) := f x in (z, r, Qred (r + snd (x, 0))))) with (snd (f x)) by (destruct (f x); unfold snd; rewrite Qred_correct; apply Qplus_0_r). setoid_replace (snd (let (z, r) := f (f x) in (z, r, Qred (r + snd (x, 0))))) with (snd (f (f x))) by (destruct (f (f x)); unfold snd; rewrite Qred_correct; apply Qplus_0_r). apply AbsSmall_Qabs. rewrite Qabs_Qminus. unfold Qminus. rewrite (Qplus_comm (snd (f x))), <- Qplus_assoc. rewrite Qplus_opp_r, Qplus_0_r. specialize (decr xH) as [decr _]. apply (Qle_trans _ _ _ decr). apply (Qle_trans _ (proj1_sig e + 0)). rewrite Qplus_0_r. exact q. apply Qplus_le_r, Qpos_nonneg. + rewrite SumStream_fst_red. unfold fst. apply Qle_bool_iff. rewrite <- iterate_shift, <- iterate_succ. specialize (lz e). revert lz. generalize (cvmod e). apply (Pos.peano_case (fun p => Qabs (Str_pth p x) <= ` e → Qabs (snd (CRstreams.iterate (X * Q) f (Pos.succ (Pos.pred p)) x)) <= ` e)). intros _. simpl. specialize (decr xH) as [decr _]. unfold Str_pth in decr. simpl in decr. apply (Qle_trans _ _ _ decr q). intros. rewrite Pos.pred_succ. apply H. + rewrite SumStream_fst_red. unfold fst. simpl. apply Qle_bool_iff. specialize (decr xH) as [decr _]. apply (Qle_trans _ _ _ decr). exact q. + rewrite SumStream_fst_red. unfold fst. apply Qle_bool_iff. apply lz. + rewrite SumStream_fst_red. unfold fst. apply Qle_bool_iff. exact q. 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