proposition: Lemma SumStream_fst_red : forall p z, fst (CRstreams.iterate _ (fun y:X*Q*Q => let (z,r) := f (fst y) in (z, r, Qred (r + snd y))) p z) ≡ CRstreams.iterate _ f p (fst z).
proof: Proof. apply (Pos.peano_ind (fun p => forall z : X * Q * Q, fst (CRstreams.iterate (X * Q * Q) (fun y : X * Q * Q => let (z0, r) := f (fst y) in (z0, r, Qred (r + snd y))) p z) ≡ CRstreams.iterate (X * Q) f p (fst z))). - intro z. simpl. destruct (f (fst z)); reflexivity. - intros. rewrite iterate_succ, H. rewrite iterate_succ. destruct (f (CRstreams.iterate (X * Q) f p (fst z))). 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