fact: Definition uc_compose_uc X Y Z : (Y-->Z)-->(X-->Y)-->X-->Z := Build_UniformlyContinuousFunction (@is_uc_uc_compose X Y Z).
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List