proposition: Lemma CR_lt_ltT x y : prod (x < y -> CRltT x y) (CRltT x y -> x < y).
proof: Proof. split. intros E. apply CR_epsilon_sign_dec_pos. apply constructive_indefinite_description_nat in E. destruct E as [n En]. now exists ((1#4) * Qpos_power (2#1) (-cast nat Z n))%Qpos. intros. now apply comparison_eq_dec. intros [ε Eε]. exists (Z.nat_of_Z (-Qdlog2 ('ε))). apply CR_epsilon_sign_dec_pos_rev. apply CRle_trans with ('proj1_sig ε); auto. apply CRle_Qle. simpl. destruct (decide (proj1_sig ε ≤ 1)). rewrite Z.nat_of_Z_nonneg. rewrite Z.opp_involutive. apply Qdlog2_spec. now destruct ε. apply Z.opp_nonneg_nonpos. now apply Qdlog2_nonpos. rewrite Z.nat_of_Z_nonpos. now apply Qlt_le_weak, Qnot_le_lt. apply Z.opp_nonpos_nonneg. apply Qdlog2_nonneg. now apply Qlt_le_weak, Qnot_le_lt. 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