proposition: Lemma err_prop_monotone' : forall (e:Q) (s: Stream Q), GeometricSeries s -> err_prop e s = true -> err_prop e (tl s) = true.
proof: Proof. intros e s Hs H. rewrite -> err_prop_prop in *. eapply Qle_trans;[|apply H]. unfold err_bound. apply Qmult_le_r. - apply Qinv_lt_0_compat. unfold Qminus. rewrite <- Qlt_minus_iff. exact Ha1. - destruct Hs as [H0 _]. eapply Qle_trans;[apply H0|]. rewrite <- (Qmult_1_l (Qabs(hd s))) at 2. apply Qmult_le_compat_r. apply Qlt_le_weak, Ha1. apply Qabs_nonneg. 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