proposition: Lemma Str_alt_decr_decr : forall (X:Type) (f : X*Q->X*Q) x (fdecr : Str_alt_decr X f x) (n : nat), 0 <= Str_pth _ f 1 x -> (-1) ^ S n * Str_pth X f (Pos.of_nat (S (S n))) x <= (-1) ^ n [*] Str_pth X f (Pos.of_nat (S n)) x.
proof: Proof. intros. pose proof (Str_alt_decr_pos X f x fdecr). specialize (fdecr (Pos.of_nat (S n))) as [fdecr _]. rewrite <- Qmult_1_l in fdecr. rewrite <- (abs_power_neg_one (S n)) in fdecr. rewrite <- (Qmult_1_l (Qabs (Str_pth X f (Pos.of_nat (S n)) x))) in fdecr. rewrite <- (abs_power_neg_one n) in fdecr. rewrite <- Qabs_Qmult, <- Qabs_Qmult in fdecr. rewrite Qabs_pos, Qabs_pos in fdecr. rewrite Nat2Pos.inj_succ. 2: discriminate. exact fdecr. apply H0, H. apply H0, 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