proposition: Lemma CR_apart_apartT x y : prod (x ≶ y -> CRapartT x y) (CRapartT x y -> x ≶ y).
proof: Proof. split. intros E. set (f (n : nat) := CR_epsilon_sign_dec ((1#4) * Qpos_power (2#1) (-cast nat Z n))). assert (∃ n, f n (y - x) ≡ Gt ∨ f n (x - y) ≡ Gt) as E2. now destruct E as [[n En] | [n En]]; exists n; [left | right]. apply constructive_indefinite_description_nat in E2. destruct E2 as [n E2]. destruct (comparison_eq_dec (f n (y - x)) Gt) as [En|En]. left. apply CR_epsilon_sign_dec_pos. now exists ((1#4) * Qpos_power (2#1) (-cast nat Z n))%Qpos. right. apply CR_epsilon_sign_dec_pos. exists ((1#4) * Qpos_power (2#1) (-cast nat Z n))%Qpos. destruct E2; tauto. intros n. destruct (comparison_eq_dec (f n (y - x)) Gt); auto. destruct (comparison_eq_dec (f n (x - y)) Gt); tauto. intros [E|E]. left. now apply CR_lt_ltT. right. now apply CR_lt_ltT. 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