proposition: Lemma CR_epsilon_sign_dec_pos_rev (x : CR) (e : Qpos) : ('proj1_sig e <= x)%CR -> CR_epsilon_sign_dec ((1#4) * e) x ≡ Gt.
proof: Proof. intros E. apply CR_epsilon_sign_dec_Gt. apply Qplus_le_l with (-proj1_sig e)%Q. simpl ((2#1) * ` ((1 # 4)%Q ↾ eq_refl * e)%Qpos + - ` e)%Q. setoid_replace ((2#1) * ((1 # 4) * proj1_sig e) + - proj1_sig e)%Q with (-((1#2) * proj1_sig e))%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). replace ((1#4) * e)%Qpos with ((1#2) * ((1#2) * e))%Qpos. now apply (E ((1#2) * e))%Qpos. apply Qpos_hprop. now destruct e as [[[ | | ] ?] ?]. 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