proposition: Lemma distConst(X : MetricSpace):forall (x:Complete X), msp_eq (dist (@constStepF (msp_as_RSetoid (Complete X)) x)) (distconst x).
proof: Proof. intros. intros e1 e2. simpl. unfold dist_raw. simpl. unfold StepFSupBall, StepFfoldProp;simpl. rewrite Qplus_0_r. apply x. 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