proposition: Lemma SumStream_init : forall (p:positive) z (r:Q), snd (CRstreams.iterate _ (fun y : X * Q * Q => let (z0, r1) := f (fst y) in (z0, r1, r1 + snd y)) p (z, r)) == r + snd (CRstreams.iterate _ (fun y : X * Q * Q => let (z0, r1) := f (fst y) in (z0, r1, r1 + snd y)) p (z, 0)).
proof: Proof. apply (Pos.peano_ind (fun p => forall (z : X * Q) (r : Q), snd (CRstreams.iterate (X * Q * Q) (fun y : X * Q * Q => let (z0, r1) := f (fst y) in (z0, r1, r1 + snd y)) p (z, r)) == r + snd (CRstreams.iterate (X * Q * Q) (fun y : X * Q * Q => let (z0, r1) := f (fst y) in (z0, r1, r1 + snd y)) p (z, 0)))). - intros. rewrite iterate_one, iterate_one. unfold fst. destruct (f z). unfold snd. rewrite Qplus_0_r. apply Qplus_comm. - intros. rewrite iterate_succ, SumStream_fst. rewrite iterate_succ, SumStream_fst. change (fst (z,r)) with z. change (fst (z,0)) with z. destruct (f (CRstreams.iterate (X * Q) f p z)). unfold snd at 1 4. rewrite H. rewrite (Qplus_comm q), <- Qplus_assoc. rewrite <- (Qplus_comm q). 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