proposition: Lemma AltSeries_correct : forall (cvmod : Qpos -> positive) (decr : Str_alt_decr _ g gInit) (xpos : 0 < snd fInit) (lz : Limit_zero _ g gInit cvmod), (ARtoCR (AltSeries cvmod decr xpos lz) == CRAlternatingSum.AltSeries _ g gInit cvmod decr lz)%CR.
proof: Proof. intros. apply regFunEq_equiv, regFunEq_e. intro d. setoid_replace (` d + ` d)%Q with (`d*(1#2) + (`d*(1#2)+` d))%Q by ring. apply (ball_triangle _ _ _ _ _ _ (AltSeries_raw_correct d cvmod xpos)). apply (AltSeries_further _ g gInit (cvmod (d * (1 # 2))%Qpos) (cvmod d) _ _ (d*(1#2))%Qpos d decr). apply lz. apply lz. apply app_inverse_below_correct. apply Qle_refl. Qed.
imports: Coq.QArith.Qabs CoRN.util.Qdlog CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric CoRN.model.reals.CRreal CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRstreams CoRN.reals.faster.ApproximateRationals CoRN.reals.faster.ARArith