fact: Definition SumStream x (p : positive) (e : Qpos) : Q := snd (iterate_stop _ (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))) (proj1_sig e)) p (x, 0)).
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