proposition: Lemma AR_lt_ltT x y : prod (x < y -> ARltT x y) (ARltT x y -> x < y).
proof: Proof. split. - intros E. apply ConstructiveEpsilon.constructive_indefinite_description_nat in E. destruct E as [n En]. now apply AR_epsilon_sign_dec_pos with (-1 - cast nat Z n). intros. now apply comparison_eq_dec. - intros [ε Eε]. exists (Z.nat_of_Z (-Qdlog2 ('ε))). apply AR_epsilon_sign_dec_pos_rev. transitivity ('ε : AR); [| assumption]. rapply (order_preserving (cast AQ AR)). apply (order_reflecting (cast AQ Q)). rewrite aq_shift_correct, rings.preserves_1, rings.mult_1_l. destruct (decide (('ε : Q) ≤ 1)). rewrite Z.nat_of_Z_nonneg. mc_setoid_replace (1 + (-1 - - Qdlog2 ('ε))) with (Qdlog2 ('ε)) by ring. apply Qdlog2_spec. apply semirings.preserves_pos. now destruct ε. change (0 ≤ -Qdlog2 ('ε)). apply rings.flip_nonpos_negate. now apply Qdlog2_nonpos. rewrite Z.nat_of_Z_nonpos. now apply orders.le_flip. change (-Qdlog2 ('ε) ≤ 0). apply rings.flip_nonneg_negate. apply Qdlog2_nonneg. now apply orders.le_flip. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program Coq.setoid_ring.Ring Coq.QArith.Qabs CoRN.stdlib_omissions.Q MathClasses.misc.workaround_tactics CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.util.Qdlog CoRN.metric2.Complete CoRN.metric2.Prelength CoRN.model.metric2.Qmetric CoRN.metric2.MetricMorphisms CoRN.reals.fast.CRArith CoRN.reals.fast.CRpower MathClasses.implementations.stdlib_binary_naturals MathClasses.orders.minmax MathClasses.implementations.positive_semiring_elements CoRN.reals.faster.ApproximateRationals CoRN.reals.faster.AQmetric