proposition: Lemma QboundAbove_uc_prf (a:Q) : is_UniformlyContinuousFunction (fun b:Q => (Qmin a b):Q) Qpos2QposInf.
proof: Proof. intros e b0 b1 H. simpl in *. unfold Qball. unfold QAbsSmall. setoid_replace (Qmin a b0 - Qmin a b1) with ((Qmax (- a) (-b1)) - (Qmax (-a) (-b0))). apply QboundBelow_uc_prf. apply Qopp_uc_prf. apply ball_sym. assumption. unfold Qminus. simpl. rewrite -> Qmin_max_de_morgan. rewrite -> Qmax_min_de_morgan. repeat rewrite -> Qopp_involutive. ring_simplify. reflexivity. Qed.
imports: QArith Qabs CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.metric2.CRmetric CoRN.model.totalorder.QMinMax CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric CoRN.stdlib_omissions.Pair MathClasses.interfaces.canonical_names