proposition: Lemma StepFSupBall_sym : forall e (x y:StepF (msp_as_RSetoid X)), (StepFSupBall e x y) -> (StepFSupBall e y x).
proof: Proof. intros e x y. unfold StepFSupBall. set (b:=(@ballS X e)). apply StepF_imp_imp. unfold StepF_imp. set (f:=ap (compose (@ap _ _ _) (compose (compose imp) b)) (flip (b))). cut (StepFfoldProp (f ^@> x <@> y)). unfold f; evalStepF; tauto. apply StepFfoldPropForall_Map2. intros a b0. simpl. unfold compose0. 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