proposition: Lemma StepFSupBall_closed : forall e (x y:StepF (msp_as_RSetoid X)), (forall d, Qlt (0#1) d -> (StepFSupBall (e+d) x y)) -> (StepFSupBall e x y).
proof: Proof. intros e. apply: (StepF_ind2). - intros. rewrite -> H, H0 in H1. apply H1. intro. rewrite -> H, H0. apply H2. - apply: ball_closed. - intros o s s0 t t0 IH0 IH1 H. unfold StepFSupBall in *. rewrite MapGlue. rewrite ApGlue. simpl. split. rewrite SplitLGlue. apply IH0. clear IH0. intros d dpos. pose (H2:=H d). rewrite -> MapGlue in H2. rewrite ApGlue in H2. rewrite SplitRGlue in H2. rewrite SplitLGlue in H2. destruct H2. exact dpos. auto. rewrite SplitRGlue. apply IH1. clear IH1. intros d dpos. pose (H2:=H d). rewrite -> MapGlue in H2. rewrite ApGlue in H2. rewrite SplitRGlue in H2. rewrite SplitLGlue in H2. destruct H2. exact dpos. auto. 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