proposition: Lemma denomPos_iter : forall p x, 0 < snd (snd x) -> 0 < snd (snd (CRstreams.iterate _ fS p x)).
proof: Proof. apply (Pos.peano_ind (fun p => forall x, 0 < snd (snd x) -> 0 < snd (snd (CRstreams.iterate _ fS p x)))). - intros. simpl. apply denomPos, H5. - intros. rewrite iterate_succ, iterate_shift. apply H5. simpl. apply denomPos, H6. 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