proposition: Lemma StepF_eq_change_base_setoid : forall s t : StepFunction.StepF Q, (@StepF_eq (msp_as_RSetoid Q_as_MetricSpace) s t) <-> (@StepF_eq QS s t).
proof: Proof. induction s. - intro t. apply StepF_eq_change_base_setoid_const. - intro t. split. + intro metricEq. apply glue_StepF_eq. apply SplitL_resp_Xeq with (a:=o) in metricEq. rewrite StepFunction.SplitLGlue in metricEq. apply IHs1 in metricEq. exact metricEq. apply SplitR_resp_Xeq with (a:=o) in metricEq. rewrite StepFunction.SplitRGlue in metricEq. apply IHs2 in metricEq. exact metricEq. + intro stdEq. apply glue_StepF_eq. apply SplitL_resp_Xeq with (a:=o) in stdEq. rewrite (StepFunction.SplitLGlue) in stdEq. apply IHs1 in stdEq. exact stdEq. apply SplitR_resp_Xeq with (a:=o) in stdEq. rewrite StepFunction.SplitRGlue in stdEq. apply IHs2 in stdEq. exact stdEq. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.structures.StepQsec CoRN.metric2.Prelength CoRN.model.metric2.L1metric CoRN.model.metric2.LinfMetricMonad CoRN.model.structures.OpenUnit Coq.QArith.QArith CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.metric2.Qmetric CoRN.algebra.COrdFields2 CoRN.tactics.CornTac