proposition: Lemma Qabs_uc_prf : is_UniformlyContinuousFunction (Qabs:Q_as_MetricSpace -> Q_as_MetricSpace) Qpos2QposInf.
proof: Proof. intros e a b Hab. simpl in *. unfold Qball in *. rewrite <- AbsSmall_Qabs in *. apply Qabs_case. intros _. eapply Qle_trans;[|apply Hab]. apply Qabs_triangle_reverse. intros _. setoid_replace (- (Qabs a - Qabs b)) with (Qabs b - Qabs a) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; ring). rewrite Qabs_Qminus in Hab. eapply Qle_trans;[|apply Hab]. apply Qabs_triangle_reverse. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRArith CoRN.model.metric2.Qmetric Coq.QArith.Qabs CoRN.model.totalorder.QMinMax CoRN.logic.Stability