proposition: Lemma ARtoCR_preserves_inv_pos_aux c (x : AR) : is_RegularFunction_noInf _ (λ γ, / Qmax (''c) ('approximate x (Qinv_modulus ('c) γ)) : Q_as_MetricSpace).
proof: Proof. intros ε1 ε2. apply_simplified (Qinv_pos_uc_prf ('c) (ε1 + ε2)%Qpos). apply AQball_fold. setoid_replace (' c * ' c * (` ε1 + ` ε2))%Q with (proj1_sig (Qinv_modulus ('c) ε1 + Qinv_modulus ('c) ε2)%Qpos) by (unfold equiv, stdlib_rationals.Q_eq; simpl; ring). apply regFun_prf. 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