proposition: Lemma Qopp_uc_prf : @is_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace Qopp Qpos2QposInf.
proof: Proof. intros e a b H. simpl in *. unfold Qball in *. apply QAbsSmall_opp in H. unfold QAbsSmall. setoid_replace (-a - - b) with (-(a-b)). apply H. 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