proposition: Lemma StepF_eq_change_base_setoid_const : forall (s : StepFunction.StepF Q) (q : Q), (@StepF_eq (msp_as_RSetoid Q_as_MetricSpace) (constStepF q) s) <-> (@StepF_eq QS (constStepF q) s).
proof: Proof. induction s. - intro q. apply Qball_0. - split. + intro metricEq. symmetry. apply (@glue_StepF_eq QS). unfold SplitL, StepFunction.SplitL. simpl. apply SplitL_resp_Xeq with (a:=o) in metricEq. rewrite (StepFunction.SplitLGlue) in metricEq. unfold StepFunction.SplitL in metricEq. simpl in metricEq. symmetry. apply (IHs1 q), metricEq. unfold SplitR, StepFunction.SplitR. simpl. apply SplitR_resp_Xeq with (a:=o) in metricEq. rewrite StepFunction.SplitRGlue in metricEq. unfold StepFunction.SplitR in metricEq. simpl in metricEq. symmetry. apply (IHs2 q), metricEq. + intro stdEq. symmetry. apply (@glue_StepF_eq (msp_as_RSetoid (Q_as_MetricSpace))). unfold SplitL, StepFunction.SplitL. simpl. apply SplitL_resp_Xeq with (a:=o) in stdEq. rewrite (StepFunction.SplitLGlue) in stdEq. unfold StepFunction.SplitL in stdEq. simpl in stdEq. symmetry. apply (IHs1 q), stdEq. unfold SplitR, StepFunction.SplitR. simpl. apply SplitR_resp_Xeq with (a:=o) in stdEq. rewrite StepFunction.SplitRGlue in stdEq. unfold StepFunction.SplitR in stdEq. simpl in stdEq. symmetry. apply (IHs2 q), 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