proposition: Lemma err_prop_tail_correct : forall (series : Stream Q) (e0 e1:Q) (p p0 : nat), GeometricSeries series -> e1 <= e0 -> err_prop e0 (Str_nth_tl p series) = true -> err_prop e1 (Str_nth_tl p0 series) = true -> Qball e0 (InfiniteSum_fat (err_prop e0) series 0%Q p) (InfiniteSum_fat (err_prop e1) series 0%Q p0).
proof: Proof. intros series e0 e1 p0 p1 H He H0 H1. pose proof (@InfiniteSum_fat_remove_filter p0 (err_prop e0) series 0%Q) as [i [H2 H3]]. exact H0. rewrite H2. pose proof (@InfiniteSum_fat_remove_filter p1 (err_prop e1) series 0%Q) as [j [H4 H5]]. exact H1. rewrite H4. clear H4 H2 H1 H0 p0 p1. destruct H3. destruct H5. destruct (Nat.lt_ge_cases j i). - exfalso. specialize (H0 j H4). pose proof (err_prop_monotone (Str_nth_tl j series) He H3) as mon. rewrite mon in H0. discriminate. - unfold Qball. rewrite <- AbsSmall_Qabs, Qabs_Qminus. apply Nat.le_exists_sub in H4. destruct H4 as [p [H4 _]]. subst j. clear H3 H2 He e1. rewrite InfiniteSum_fat_minus. apply err_prop_correct. 2: exact H1. apply ForAll_Str_nth_tl, H. 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