proposition: Lemma err_prop_key' : forall (e:Q) (s: Stream Q), GeometricSeries s -> err_prop e s = true -> err_prop (a*e) (tl s) = true.
proof: Proof. intros e s [H _] Hs. rewrite -> err_prop_prop in *. unfold err_bound in *. rewrite -> Qle_minus_iff in H, Hs |- *. rewrite -> Qlt_minus_iff in Ha1. setoid_replace (a * e + - (Qabs (hd (tl s)) / (1 - a))) with (a * (e + - (Qabs (hd s)/(1-a)))+ (a * Qabs (hd s) + - Qabs (hd (tl s)))/(1+-a)) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; field). rewrite <- Qplus_0_r. apply Qplus_le_compat. apply Qmult_le_0_compat. exact Ha0. exact Hs. apply Qmult_le_0_compat. exact H. apply Qlt_le_weak, Qinv_lt_0_compat, Ha1. intro abs. rewrite abs in Ha1. exact (Qlt_irrefl 0 Ha1). 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