proposition: Lemma err_prop_correct : forall (p:nat) (e:Q) (s : Stream Q) (e':Stream Q -> bool), GeometricSeries s -> err_prop e s = true -> Qabs (InfiniteSum_fat e' s 0%Q p) <= e.
proof: Proof. induction p. - intros. simpl. apply err_prop_nonneg in H0. destruct (e' s); exact H0. - intros. simpl. destruct (e' s). apply err_prop_nonneg in H0. exact H0. rewrite InfiniteSum_fat_plus. rewrite Qplus'_correct, Qplus_0_l. rewrite <- Qplus'_correct. apply err_prop_key. exact H0. apply (IHp (a*e)). apply H. apply err_prop_key'; 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