proposition: Lemma fSsum_fst : forall p k, fst (CRstreams.iterate _ (fSsum k) p (1%positive, fInit, 0)) ≡ CRstreams.iterate _ fS p (xH,fInit).
proof: Proof. apply (Pos.peano_ind (fun p => forall k, fst (CRstreams.iterate _ (fSsum k) p (1%positive, fInit, 0)) ≡ CRstreams.iterate _ fS p (xH,fInit))). - reflexivity. - intros. rewrite iterate_succ, iterate_succ. rewrite <- (H5 k). unfold fSsum at 1. destruct (CRstreams.iterate ((positive and AQ and AQ) and AQ) (fSsum k) p (1%positive, fInit, 0)). reflexivity. Qed.
imports: Coq.QArith.Qabs CoRN.util.Qdlog CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric CoRN.model.reals.CRreal CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRstreams CoRN.reals.faster.ApproximateRationals CoRN.reals.faster.ARArith