fact: Definition InfiniteGeometricSum_shift_raw (s : Stream Q) (n : nat) {a : Q} (Gs : GeometricSeries a (Str_nth_tl n s)) (e : QposInf) : Q := take s n Qplus' 0 + InfiniteGeometricSum_raw a (Str_nth_tl n s) e.
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