proposition: Lemma Limit_zero_tl : forall x (cvmod : Qpos -> positive) (p : positive), Str_alt_decr x -> Limit_zero x cvmod -> Limit_zero (CRstreams.iterate _ f p x) (fun e => cvmod e - p)%positive.
proof: Proof. intros. intro e. unfold Str_pth. rewrite <- iterate_add. assert (forall q:positive, Qabs (snd (CRstreams.iterate (X * Q) f (q+cvmod e) x)) <= ` e). { apply Pos.peano_ind. - intros. rewrite Pos.add_1_l. apply (Qle_trans _ (Qabs (snd (CRstreams.iterate (X * Q) f (cvmod e) x)))). apply H. apply H0. - intros. rewrite <- Pos.add_1_l, <- Pos.add_assoc, Pos.add_1_l. refine (Qle_trans _ _ _ _ H1). apply H. } destruct (Pos.lt_total p (cvmod e)). 2: destruct H2. - rewrite Pos.sub_add. apply H0. exact H2. - subst p. rewrite Pos.sub_diag. apply H1. - rewrite Pos.sub_lt. 2: exact H2. replace (1+p)%positive with (1+(p-cvmod e)+cvmod e)%positive. apply H1. rewrite <- Pos.add_assoc. apply f_equal. rewrite Pos.sub_add. reflexivity. exact H2. Qed.
imports: Coq.setoid_ring.ArithRing Coq.Bool.Bool Coq.QArith.Qpower Coq.QArith.Qabs CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.model.metric2.Qmetric CoRN.reals.fast.LazyNat CoRN.reals.fast.CRstreams CoRN.metric2.Limit CoRN.model.totalorder.QposMinMax CoRN.classes.Qclasses MathClasses.interfaces.abstract_algebra