proposition: Lemma SumStream_shift : forall p x e, ` e < Qabs (snd (f x)) -> snd (f x) + SumStream (f x) p e == SumStream x (Pos.succ p) e.
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))) (` e)) p (f x,0)) as [s [seq [H0 H1]]]. rewrite seq, SumStream_red. pose proof (SumStream_assoc x 1 s) as H2. rewrite iterate_one, iterate_one in H2. setoid_replace (snd (f x)) with (snd (let (z, r0) := f (fst (x, 0)) in (z, r0, r0 + snd (x, 0)))) by (simpl; destruct (f x); simpl; rewrite Qplus_0_r; reflexivity). rewrite <- H2. clear H2. rewrite Pos.add_1_l. 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))) (` e)) (Pos.succ p) (x,0)) as [r [req [H2 H3]]]. rewrite req, SumStream_red. clear req seq. assert (r ≢ 1%positive) as rone. { intro abs. clear H2 H0 H1. subst r. destruct H3. pose proof (Pos.lt_1_succ p). rewrite H0 in H1. inversion H1. destruct H0. rewrite SumStream_fst_red in H1. simpl in H1. apply Qle_bool_iff in H1. exact (Qlt_not_le _ _ H H1). } destruct H1 as [finish|stop]. - subst s. destruct H3. subst r. reflexivity. exfalso. destruct H1. apply Qle_bool_iff in H3. rewrite SumStream_fst_red in H3. unfold fst in H3. rewrite <- (Pos.succ_pred r) in H1. 2: exact rone. apply Pos.succ_lt_mono in H1. specialize (H0 (Pos.pred r) H1). rewrite SumStream_fst_red in H0. unfold fst in H0. rewrite <- iterate_shift, <- iterate_succ, Pos.succ_pred in H0. apply Qle_bool_iff in H3. rewrite H0 in H3. discriminate. exact rone. - destruct stop. rewrite SumStream_fst_red in H4. unfold fst in H4. rewrite <- iterate_shift, <- iterate_succ in H4. destruct H3. exfalso. subst r. apply Pos.succ_lt_mono in H1. specialize (H2 (Pos.succ s) H1). rewrite SumStream_fst_red in H2. unfold fst in H2. rewrite H4 in H2. discriminate. destruct (Pos.lt_total r (Pos.succ s)). exfalso. destruct H3. rewrite SumStream_fst_red in H6. unfold fst in H6. rewrite <- (Pos.succ_pred r) in H5. 2: exact rone. apply Pos.succ_lt_mono in H5. specialize (H0 _ H5). rewrite SumStream_fst_red in H0. unfold fst in H0. rewrite <- iterate_shift, <- iterate_succ, Pos.succ_pred in H0. rewrite H0 in H6. discriminate. exact rone. destruct H5. rewrite H5. reflexivity. exfalso. specialize (H2 (Pos.succ s) H5). rewrite SumStream_fst_red in H2. unfold fst in H2. rewrite H4 in H2. discriminate. 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