proposition: Lemma AQinv_pos_uc_prf (c : AQ₊) : is_UniformlyContinuousFunction (AQinv_bounded c) (Qinv_modulus ('c)).
proof: Proof. intros ε x y E δ1 δ2. simpl in *. eapply ball_triangle. 2: now eapply ball_sym, aq_div_dlog2. eapply ball_triangle. now eapply aq_div_dlog2. simpl. aq_preservation. rewrite 2!left_identity. pose proof (Qinv_pos_uc_prf (' c) ε (' x) (' y)) as H5. simpl in H5. apply H5. exact E. 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