proposition: Lemma InfiniteGeometricSum_small_tail : forall series (e : Qpos), GeometricSeries series -> {n : nat & forall Gs : GeometricSeries (Str_nth_tl n series), (- ' proj1_sig e <= InfiniteGeometricSum Gs /\ InfiniteGeometricSum Gs <= 'proj1_sig e)%CR }.
proof: Proof. intros series e. exists (nat_of_P (InfiniteGeometricSum_maxIter series e)). intros Gs. pose proof (InfiniteGeometricSum_bound Gs) as [H0 H1]. split. refine (CRle_trans _ H0). apply CRopp_le_compat. rewrite -> CRle_Qle. rewrite <- err_prop_prop. apply InfiniteGeometricSum_maxIter_correct. assumption. apply (CRle_trans H1). rewrite -> CRle_Qle. rewrite <- err_prop_prop. apply InfiniteGeometricSum_maxIter_correct. assumption. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRstreams CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax Coq.QArith.Qpower Coq.QArith.Qabs Coq.ZArith.Zdiv