proposition: Lemma inject_Q_AR_prf : forall (q:Q), is_RegularFunction (@ball AQ_as_MetricSpace) (fun e:QposInf => match e with | Qpos2QposInf d => app_inverse (cast AQ Q) q d | QposInfinity => 0 end).
proof: Proof. intros q e1 e2. simpl. destruct aq_dense_embedding. simpl in dense_inverse. unfold cast. apply (ball_triangle _ _ _ _ q). apply dense_inverse. apply ball_sym, dense_inverse. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program Coq.setoid_ring.Ring CoRN.util.Qdlog CoRN.model.totalorder.QposMinMax CoRN.metric2.Complete CoRN.metric2.Prelength CoRN.model.metric2.Qmetric CoRN.model.metric2.CRmetric CoRN.metric2.MetricMorphisms CoRN.reals.faster.ApproximateRationals