proposition: Lemma AltSeries_remainder : forall (X : Type) (f : X * Q → X * Q) (x : X * Q) (cvmod : Qpos → positive) (fdecr : Str_alt_decr X f x) (flz : Limit_zero X f x cvmod) (e : CRasCReals) (p : positive), AbsSmall e (' Str_pth X f p x)%CR -> AbsSmall e (inject_Q_CR (snd (CRstreams.iterate ((X and Q) and Q) (λ y : (X and Q) and Q, let (z0, r1) := f (fst y) in (z0, r1, Qred (r1 + snd y))) p (x, 0%Q))) - AltSeries X f x cvmod fdecr flz)%CR.
proof: Proof. intros. rewrite (AltSeries_shift_pth p). rewrite CRopp_plus_distr, CRplus_assoc. rewrite CRplus_opp. apply (AbsSmall_minus CRasCOrdField e _ 0%CR). unfold cg_minus. simpl. rewrite CRopp_0, CRplus_0_r. apply AltSeries_small_inf. specialize (fdecr p) as [fdecr _]. unfold Str_pth in fdecr. rewrite <- CRstreams.iterate_succ. apply CRabs_AbsSmall. rewrite inject_Q_CR_abs. apply (@CRle_trans _ (inject_Q_CR (Qabs (snd (CRstreams.iterate (X and Q) f p x))))). apply (order_embedding_preserving inject_Q_CR), fdecr. rewrite <- inject_Q_CR_abs. apply CRabs_AbsSmall. apply H. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.iso_CReals CoRN.reals.Q_in_CReals Coq.setoid_ring.ArithRing CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.fast.CRabs Coq.Bool.Bool CoRN.algebra.COrdAbs CoRN.model.ordfields.Qordfield CoRN.model.metric2.Qmetric CoRN.reals.fast.LazyNat CoRN.metric2.Limit CoRN.model.totalorder.QposMinMax Coq.QArith.Qpower Coq.QArith.Qabs MathClasses.theory.CoqStreams CoRN.transc.PowerSeries CoRN.tactics.CornTac CoRN.classes.Qclasses MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.series MathClasses.theory.streams CoRN.reals.fast.CRAlternatingSum