fact: Fixpoint InfiniteSum_raw_N (n:nat) (filter: Stream Q -> bool) (cont: Stream Q -> Q -> Q) {struct n} : Stream Q -> Q -> Q := match n with | O => InfiniteSum_raw_F cont filter | S p => InfiniteSum_raw_N p filter (fun s => InfiniteSum_raw_N p filter cont s) 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