proposition: Lemma Qmax_uc_prf : is_UniformlyContinuousFunction QboundBelow_uc Qpos2QposInf.
proof: Proof. intros e a0 a1 H. split. apply Qpos_nonneg. intro b. simpl in *. do 2 rewrite -> (fun x => Qmax_comm x b). apply QboundBelow_uc_prf. 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