proposition: Lemma ARtoCR_preserves_pos x : prod (ARpos x -> CRpos ('x)) (CRpos ('x) -> ARpos x).
proof: Proof. Proof with auto with qarith. split; intros [y E]. exists (cast (AQ₊) (Q₊) y). change (cast Q CR (cast AQ Q (cast (AQ₊) AQ y)) ≤ cast AR CR x). rewrite <-ARtoCR_inject. now apply (order_preserving _). destruct (aq_lt_mid 0 (proj1_sig y)) as [z [Ez1 Ez2]]... assert (0 < z) as F. apply (strictly_order_reflecting (cast AQ Q)). now aq_preservation... exists (exist _ z F). simpl. change (cast AQ AR (cast (AQ₊) AQ (z ↾ F)) ≤ x). apply (order_reflecting (cast AR CR)). rewrite ARtoCR_inject. transitivity (cast Q CR (cast Qpos Q y)); trivial. apply CRle_Qle... Defined.
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