fact: Definition uneven_CRplus: CR := @mkRegularFunction Q_as_MetricSpace 0 _ uneven_CRplus_is_RegularFunction.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.QArith CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric CoRN.reals.fast.CRArith