proposition: Lemma err_prop_key : forall (e:Q) (s: Stream Q) (x:Q), err_prop e s = true -> Qabs x <= a*e -> Qabs (Qplus' (hd s) x) <= e.
proof: Proof. intros e s x Hs Hx. rewrite -> Qplus'_correct. eapply Qle_trans. apply Qabs_triangle. setoid_replace e with (e*(1-a) + a*e) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). assert (X:0 < 1 - a). change (0 < 1 + - a). rewrite <- Qlt_minus_iff. assumption. apply Qplus_le_compat; try assumption. rewrite -> err_prop_prop in Hs. unfold err_bound in Hs. apply Qmult_lt_0_le_reg_r with (/(1-a)). apply Qinv_lt_0_compat; assumption. rewrite <- Qmult_assoc, Qmult_inv_r, Qmult_1_r. assumption. auto with *. 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