proposition: Lemma dist_glue(X:MetricSpace)(o:OpenUnit): forall (x y:(StepFSup (Complete X))), msp_eq (dist (glue o x y)) (Cmap2_slow (glue_uc _ o) (dist x) (dist y)).
proof: Proof. pose (exist (Qlt 0) (1#2) eq_refl) as half. intros. simpl. intros e e1. simpl. unfold dist_raw. simpl. unfold Cmap_slow_fun. simpl. unfold Cap_slow_raw. simpl. unfold dist_raw. rewrite -> (StepFSupBallGlueGlue _ (proj1_sig e + 0 + proj1_sig e1) o (Map (fun z : RegularFunction (ball (m:=X)) => approximate z e) x) (Map (fun z : RegularFunction (ball (m:=X)) => approximate z e) y)). assert (forall w:StepF (msp_as_RSetoid (Complete X)), StepFSupBall (X:=X) (proj1_sig e + proj1_sig e1) (Map (fun z : RegularFunction (@ball X) => approximate z e) w) (Map (fun z : RegularFunction (@ball X) => approximate z (half * (half * e1))%Qpos) w)). induction w. unfold StepFSupBall. unfold StepFfoldProp. simpl. rewrite <- ball_Cunit. apply ball_triangle with x0. apply ball_approx_l. apply ball_weak_le with (proj1_sig (half * (half * e1))%Qpos). rewrite -> Qle_minus_iff. simpl. replace RHS with ((3#4)*proj1_sig e1); [| simpl; ring]. Qauto_nonneg. apply ball_approx_r. simpl. rewrite -> (StepFSupBallGlueGlue _ (proj1_sig e + proj1_sig e1) o0 (Map (fun z : RegularFunction (ball (m:=X)) => approximate z e) w1) (Map (fun z : RegularFunction (ball (m:=X)) => approximate z e) w2) (Map (fun z : RegularFunction (ball (m:=X)) => approximate z (half * (half * e1))%Qpos) w1) (Map (fun z : RegularFunction (ball (m:=X)) => approximate z (half * (half * e1))%Qpos) w2)). intuition. rewrite Qplus_0_r. split; apply H. 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