fact: Definition InfiniteSum_raw_F (cont: Stream Q -> Q -> Q) (err_prop:Stream Q -> bool) (s:Stream Q) (q : Q) : Q := if (err_prop s) then q else cont (tl s) (Qplus' q (hd s)).
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRstreams CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax Coq.QArith.Qpower Coq.QArith.Qabs Coq.ZArith.Zdiv