proposition: Lemma inject_Q_AR_uc : is_UniformlyContinuousFunction inject_Q_AR Qpos2QposInf.
proof: Proof. intros d e1 e2 bd x y. simpl. unfold cast. unfold MetricMorphisms.app_inverse. destruct aq_dense_embedding. unfold MetricMorphisms.app_inverse in dense_inverse. rewrite <- (Qplus_assoc (`x) (`d) (`y)). apply ball_triangle with (b:=e1). apply dense_inverse. apply ball_triangle with (b:=e2). apply bd. 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