fact: Definition ball_ex (X: MetricSpace) (e: QposInf): X -> X -> Prop := match e with | Qpos2QposInf e' => ball (proj1_sig e') | QposInfinity => fun a b => True end.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List