proposition: Lemma distreturn: forall X, (ucEq (uc_compose dist (StFReturn_uc _)) (@Cmap_slow _ _ (StFReturn_uc X))).
proof: Proof. pose (exist (Qlt 0) (1#2) eq_refl) as half. intros X x. simpl. unfold StFReturn_uc. intros e e1. simpl. unfold dist_raw. simpl. unfold StepFSupBall. change (ballS X (proj1_sig e + 0 + proj1_sig e1) (approximate x e) (approximate x (half * e1)%Qpos)). simpl. rewrite Qplus_0_r. apply ball_weak_le with (proj1_sig (Qpos_plus e (half * e1)%Qpos)). 2: apply (regFun_prf_ex x e (half * e1)%Qpos). rewrite -> Qle_minus_iff. simpl. replace RHS with ((1#2)* proj1_sig e1); [| simpl; ring]. Qauto_nonneg. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.metric2.StepFunctionMonad CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.metric2.Complete CoRN.model.metric2.LinfMetricMonad CoRN.metric2.StepFunctionSetoid CoRN.tactics.Qauto