proposition: Lemma CRnonNeg_criterion (x: CR): (forall q, (x <= ' q)%CR -> 0 <= q)%Q -> CRnonNeg x.
proof: Proof. Proof with auto with qarith. unfold CRle. unfold CRnonNeg. intros. apply Q.Qplus_le_l with (proj1_sig e). ring_simplify. apply H. intros. rewrite approximate_CRminus. simpl. cut (approximate x ((1 # 2) * e0)%Qpos - approximate x e <= proj1_sig e0 + proj1_sig e)%Q. - intros. apply Q.Qplus_le_l with (proj1_sig e0 + approximate x ((1#2)*e0)%Qpos - approximate x e)%Q. simpl. ring_simplify... - apply Qle_trans with (Qabs (approximate x ((1 # 2) * e0)%Qpos - approximate x e))%Q. apply Qle_Qabs. apply Qle_trans with (proj1_sig ((1#2)*e0)%Qpos + proj1_sig e)%Q... pose proof (regFun_prf x ((1#2)*e0)%Qpos e). apply Qball_Qabs in H0... apply Qplus_le_compat. simpl. rewrite <- (Qmult_1_r (proj1_sig e0)) at 2. rewrite (Qmult_comm (proj1_sig e0)). apply Qmult_le_compat_r... apply Qle_refl. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders