proposition: Lemma StepFSupPrelengthSpace : PrelengthSpace X -> PrelengthSpace StepFSup.
proof: Proof. intros pl. apply: StepF_ind2. intros s s0 t t0 Hs Ht H e d1 d2 He H0. rewrite <- Hs, <- Ht in H0. destruct (H _ _ _ He H0) as [c Hc0 Hc1]. exists c. rewrite <- Hs; auto. rewrite <- Ht; auto. intros a b e d1 d2 He Hab. destruct (pl a b e d1 d2 He Hab) as [c Hc0 Hc1]. exists (@constStepF (msp_as_RSetoid X) c); auto. intros o s s0 t t0 IHl IHr e d1 d2 He H. simpl in H. rewrite -> StepFSupBallGlueGlue in H. destruct H as [Hl Hr]. destruct (IHl _ _ _ He Hl) as [c Hc0 Hc1]. destruct (IHr _ _ _ He Hr) as [d Hd0 Hd1]. exists (glue o c d); simpl; rewrite -> StepFSupBallGlueGlue; 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