fact: Definition InfiniteGeometricSum_maxIter series (err:Qpos) : positive := let x := (1-a) in let (n,d) := (Qabs (hd series))/(proj1_sig err*x*x) in match Z.succ (Z.div n (Zpos d)) with | Zpos p => p | _ => 1%positive end.
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