proposition: Lemma AltSeries_convergent : forall (X:Type) (f : X*Q->X*Q) x cvmod (fdecr : Str_alt_decr X f x) (flz : Limit_zero X f x cvmod), convergent (fun n:nat => inj_Q IR (Str_pth _ f (Pos.of_nat (S n)) x)).
proof: Proof. intros. destruct (Qlt_le_dec (Str_pth _ f 1 x) 0). 2: exact (AltSeries_convergent_pos X f x cvmod fdecr flz q). apply (convergent_wd (fun n : nat => [--][1][*]inj_Q IR (Str_pth _ (CRstreams.CRstream_opp X f) (Pos.of_nat (S n)) (let (y,r):=x in (y,-r))))). - intro n. pose proof (CRstreams.CRstream_opp_pth X f x (Pos.of_nat (S n))). unfold Str_pth. destruct (CRstreams.iterate _ (CRstreams.CRstream_opp X f) (Pos.of_nat (S n)) (let (y, r) := x in (y, - r))), (CRstreams.iterate (X and Q) f (Pos.of_nat (S n)) x). unfold snd. destruct H as [_ H]. subst q0. rewrite (inj_Q_inv IR q1), inv_mult_invol. rewrite <- inj_Q_One, <- inj_Q_mult. apply inj_Q_wd, Qmult_1_l. - apply conv_series_mult_scal. apply (AltSeries_convergent_pos X (CRstreams.CRstream_opp X f) (let (y, r) := x in (y, - r)) cvmod). apply CRstream_opp_decr, fdecr. apply CRstream_opp_limit_zero, flz. unfold CRstreams.CRstream_opp, Str_pth; simpl. destruct x. unfold Str_pth in q; simpl in q. replace (--q0) with q0. destruct (f (x,q0)). unfold snd. unfold snd in q. apply (Qopp_le_compat q1 0), Qlt_le_weak, q. destruct q0. unfold Qopp; simpl. rewrite Z.opp_involutive. 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