proposition: Lemma InfiniteSum_raw_N_unfold : forall n cont (filter : Stream Q -> bool) s, InfiniteSum_raw_N (S (S n)) filter cont s = InfiniteSum_raw_N n filter (fun s0 => InfiniteSum_raw_N n filter (fun s1 => InfiniteSum_raw_N (S n) filter cont s1) s0) s.
proof: Proof. reflexivity. Qed.
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