fact: Definition CRsum_list (l:list CR) : CR := Build_RegularFunction (CRsum_list_prf l).
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRArith CoRN.stdlib_omissions.List CoRN.model.metric2.Qmetric