proposition: Lemma AltSeries_small_inf : 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), AbsSmall e (' snd (f x))%CR -> AbsSmall e (AltSeries X f x cvmod fdecr flz)%CR.
proof: Proof. intros. apply CRabs_AbsSmall. apply CRabs_AbsSmall in H. rewrite inject_Q_CR_abs in H. refine (CRle_trans _ H). clear H e. intro e. simpl. unfold Cap_raw; simpl. apply (Qle_trans _ 0%Q). apply (Qopp_le_compat 0), Qpos_nonneg. unfold Qminus. rewrite <- Qle_minus_iff. generalize (Qpos_mult (@exist Q (Qlt {| Qnum := Z0; Qden := xH |}) {| Qnum := Zpos xH; Qden := xO xH |} (@eq_refl Datatypes.comparison Datatypes.Lt)) e). clear e. intro e. unfold SumStream. pose proof (CRstreams.iterate_stop_correct _ (λ y : X * Q * Q, let (z, r) := f (fst y) in (z, r, Qred (r + snd y))) (λ y : X * Q * Q, Qle_bool (Qabs (snd (fst y))) (proj1_sig e)) (cvmod e) (x,0%Q)) as [s [seq [_ H4]]]. unfold zero, Q_0. rewrite seq. clear seq. rewrite SumStream_red. apply (AltSeries_small X f x s). exact fdecr. 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