proposition: Lemma AR_apart_apartT x y : prod (x ≶ y -> ARapartT x y) (ARapartT x y -> x ≶ y).
proof: Proof. split. - intros E. set (f (n : nat) := AR_epsilon_sign_dec (-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 ConstructiveEpsilon.constructive_indefinite_description_nat in E2. destruct E2 as [n E2]. destruct (comparison_eq_dec (f n (y - x)) Gt) as [En|En]. left. now apply AR_epsilon_sign_dec_pos with (-1 - cast nat Z n). right. apply AR_epsilon_sign_dec_pos with (-1 - cast nat Z n). 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 AR_lt_ltT. right. now apply AR_lt_ltT. 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