proposition: Lemma ARtoCR_preserves_inv_pos x c : 'ARinv_pos c x = CRinv_pos ('c) ('x).
proof: Proof. apply regFunEq_equiv, regFunEq_e. intros ε. simpl. unfold Cjoin_raw. simpl. setoid_replace (proj1_sig ε + proj1_sig ε)%Q with (proj1_sig ((1#2) * ε + ((1#2) * ε + ε)))%Qpos by (unfold equiv, stdlib_rationals.Q_eq; simpl; ring). eapply ball_triangle. now apply aq_div_dlog2. simpl. rewrite aq_preserves_max. rewrite rings.preserves_1. rewrite Qmult_1_l. change (Qball ( (1 # 2) * ` ε + ` ε) (/ Qmax (' (' c)) (' approximate x (Qinv_modulus (' c) ((1 # 2) ↾ eq_refl * ε))))%mc ( / Qmax (' c) (' approximate x (Qinv_modulus (' c) ε)))). apply (ARtoCR_preserves_inv_pos_aux c x ((1 # 2) * ε)%Qpos). 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