proposition: Lemma err_prop_nonneg : forall e s, err_prop e s = true -> 0 <= e.
proof: Proof. intros. apply err_prop_prop in H. refine (Qle_trans _ _ _ _ H). apply Qmult_le_0_compat. apply Qabs_nonneg. apply Qlt_le_weak, Qinv_lt_0_compat. unfold Qminus. rewrite <- Qlt_minus_iff. exact 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