proposition: Lemma SumStream_assoc : forall x (p q : positive), snd (CRstreams.iterate _ (fun y : X * Q * Q => let (z, r0) := f (fst y) in (z, r0, r0 + snd y)) (p+q) (x,0)) == snd (CRstreams.iterate _ (fun y : X * Q * Q => let (z, r0) := f (fst y) in (z, r0, r0 + snd y)) p (x,0)) + snd (CRstreams.iterate _ (fun y : X * Q * Q => let (z, r0) := f (fst y) in (z, r0, r0 + snd y)) q (CRstreams.iterate _ f p x, 0)).
proof: Proof. intros x p. revert p x. apply (Pos.peano_ind (fun p => forall x q, snd (CRstreams.iterate (X * Q * Q) (fun y : X * Q * Q => let (z, r0) := f (fst y) in (z, r0, r0 + snd y)) (p + q) (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 (CRstreams.iterate (X * Q * Q) (fun y : X * Q * Q => let (z, r0) := f (fst y) in (z, r0, r0 + snd y)) q (CRstreams.iterate _ f p x, 0)))). - intros x q. rewrite Pos.add_comm, iterate_add. simpl. destruct (f x) as [z r0]. rewrite SumStream_init. reflexivity. - intros. rewrite <- Pos.add_1_r, <- Pos.add_assoc, Pos.add_1_l. rewrite H, H. simpl. rewrite <- Qplus_assoc. apply Qplus_comp. reflexivity. clear H. rewrite iterate_add. simpl. rewrite <- iterate_shift. rewrite <- Pos.add_1_r, iterate_add. simpl. destruct (f (CRstreams.iterate (X * Q) f p x)). simpl. rewrite SumStream_init. reflexivity. 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