proposition: Lemma CR_epsilon_sign_dec_pos : forall x, {e:Qpos | CR_epsilon_sign_dec e x ≡ Gt} -> CRpos x.
proof: Proof. intros x [e H]. apply (@CRpos_char e). abstract (unfold CR_epsilon_sign_dec in H; destruct (Q.Qle_dec ((2#1) * proj1_sig e) (approximate x e)) as [A|A]; [assumption | destruct (Q.Qle_dec (approximate x e) (- (2#1) * proj1_sig e)) as [B|B]; discriminate H]). Defined.
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