proposition: Lemma QboundBelow_uc_prf (a:Q) : is_UniformlyContinuousFunction (fun b:Q => (Qmax a b):Q) Qpos2QposInf.
proof: Proof. intros e b0 b1 H. simpl in *. assert (X:forall a b0 b1, Qball (proj1_sig e) b0 b1 -> b0 <= a <= b1 -> Qball (proj1_sig e) a b1). clear a b0 b1 H. intros a b0 b1 H [H1 H2]. unfold Qball in *. unfold QAbsSmall in *. split. apply Qle_trans with (b0-b1). apply H. apply Qplus_le_l. assumption. apply Qle_trans with 0. apply (Qplus_le_l _ _ b1). ring_simplify. assumption. apply Qpos_nonneg. do 2 apply Qmax_case; intros H1 H2. apply ball_refl. apply Qpos_nonneg. eapply X. apply H. tauto. apply ball_sym. apply X with b1. apply ball_sym. apply H. tauto. assumption. 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