proposition: Lemma StepFSupBall_is_MetricSpace : is_MetricSpace (@StepFSupBall X).
proof: Proof. split. - intros. intro x. apply StepFSupBall_refl, H. - apply: StepFSupBall_sym. - apply: StepFSupBall_triangle. - apply: StepFSupBall_closed. - exact StepFSupBall_nonneg. - exact StepFSupBall_stable. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.metric2.StepFunctionSetoid CoRN.metric2.StepFunctionMonad CoRN.metric2.UniformContinuity CoRN.model.structures.OpenUnit Coq.QArith.QArith CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.metric2.Qmetric CoRN.metric2.Prelength CoRN.algebra.COrdFields2 CoRN.tactics.CornTac