proposition: Lemma StepFSupBall_refl : forall (e:Q) (x:StepF (msp_as_RSetoid X)), Qle (0#1) e -> StepFSupBall e x x.
proof: Proof. intros e x epos. unfold StepFSupBall. set (b:=(@ballS X e)). set (f:=(@join _ _) ^@> (constStepF b)). cut (StepFfoldProp (f <@> x )). unfold f. evalStepF. auto. apply: StepFfoldPropForall_Map. simpl. auto with *. 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