proposition: Lemma CRneg_nonPos : forall x, CRneg x -> CRnonPos x.
proof: Proof. intros x [c Hx]. cut (x <= 0)%CR. unfold CRle. intros H. assert (0 - x == -x)%CR. ring. rewrite -> H0 in H. intros e. rewrite <- (Qopp_involutive (proj1_sig e)). rewrite <- (Qopp_involutive (approximate x e)). apply Qopp_le_compat. apply H. apply CRle_trans with ('(-proj1_sig c)%Q)%CR; auto with *. rewrite -> CRle_Qle. apply (Qopp_le_compat 0). apply Qpos_nonneg. 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