proposition: Lemma fS_fst : forall (p:positive) x, fst (CRstreams.iterate (positive and AQ and AQ) fS p (1%positive, x)) ≡ Pos.succ p.
proof: Proof. apply (Pos.peano_ind (fun p => forall (x : AQ and AQ), fst (CRstreams.iterate (positive and AQ and AQ) fS p (1%positive, x)) ≡ Pos.succ p)). - reflexivity. - intros. rewrite iterate_succ. simpl. apply f_equal, H5. 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