proposition: Lemma err_prop_prop : forall e s, err_prop e s = true <-> err_bound s <= e.
proof: Proof. intros e s. unfold err_prop, err_bound, Qcompare, Qle, Z.le. destruct (Qnum (Qabs (hd s) / (1 - a))%Q * Zpos (Qden e) ?= Qnum e * Zpos (Qden (Qabs (hd s) / (1 - a))%Q))%Z; split; 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