proposition: Lemma dist_prf : forall (x:StepFSup (Complete X)), is_RegularFunction (@ball (StepFSup X)) (dist_raw x).
proof: Proof. unfold dist_raw. intros x a b. induction x. - apply (@regFun_prf _ (@ball X)). - simpl (ball (m:=StepFSup X)). set (f:=(fun z : RegularFunction (@ball X) => approximate z a)) in *. set (g:=(fun z : RegularFunction (@ball X) => approximate z b)) in *. simpl. setoid_rewrite (StepFSupBallGlueGlue). auto. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.metric2.StepFunctionMonad CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.metric2.Complete CoRN.model.metric2.LinfMetricMonad CoRN.metric2.StepFunctionSetoid CoRN.tactics.Qauto