proposition: Lemma AltSeries_convergent_0 : forall (X:Type) (f : X*Q->X*Q) x cvmod q (fdecr : Str_alt_decr X f x) (flz : Limit_zero X f x cvmod), convergent (fun n:nat => match n with | O => q | S _ => inj_Q IR (Str_pth _ f (Pos.of_nat n) x) end).
proof: Proof. intros. apply (join_series (fun n : nat => inj_Q IR (Str_pth _ f (Pos.of_nat (S n)) x))). - exact (AltSeries_convergent X f x cvmod fdecr flz). - exists 1%nat. exists O. intros n _. rewrite Nat.add_comm. reflexivity. 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