proposition: Lemma reverseRegFun : forall (x : CR) (e1 e2 : Qpos), (-(`e1+`e2) <= Qabs (approximate x e1) - Qabs (approximate x e2))%Q.
proof: Proof. intros. setoid_replace (Qabs (approximate x e1) - Qabs (approximate x e2))%Q with (-(Qabs (approximate x e2) - Qabs (approximate x e1)))%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). apply Qopp_le_compat. apply (Qle_trans _ _ _ (Qabs_triangle_reverse _ _)). pose proof (regFun_prf x e2 e1). apply AbsSmall_Qabs in H. rewrite Qplus_comm. exact H. 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