proposition: Lemma StepFSupBall_eq : forall (x y : StepF (msp_as_RSetoid X)), (forall e : Qpos, StepFSupBall (proj1_sig e) x y) -> StepF_eq x y.
proof: Proof. apply: (StepF_ind2). - intros s s0 t t0 H H0 H1 H2. rewrite -> H, H0 in H1. apply H1. intro. rewrite -> H, H0. apply H2. - intros. apply ball_eq. intros. specialize (H (exist _ _ H0)). exact H. - intros o s s0 t t0 H H0 H1. unfold StepFSupBall in *. apply glue_resp_StepF_eq. apply H. clear H. intro e. pose (H2:=H1 e). rewrite -> MapGlue in H2. rewrite ApGlue in H2. rewrite SplitRGlue in H2. rewrite SplitLGlue in H2. destruct H2; auto. apply H0. clear H0. intro e. pose (H2:=H1 e). rewrite -> MapGlue in H2. rewrite ApGlue in H2. rewrite SplitRGlue in H2. rewrite SplitLGlue in H2. destruct H2; 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