proposition: Lemma dist1_uc : is_UniformlyContinuousFunction dist1 Qpos2QposInf.
proof: Proof. intros e. apply: StepF_ind2. simpl (ball_ex). intros s s0 t t0 Hs Ht H. unfold ball_ex. apply StepF_eq_equiv in Hs. apply StepF_eq_equiv in Ht. rewrite <- Hs, <- Ht. assumption. intros. assumption. intros o s s0 t t0 Hl Hr H d1 d2. simpl. unfold dist_raw. simpl. simpl in *. rewrite -> (StepFSupBallGlueGlue _ (proj1_sig d1 + proj1_sig e + proj1_sig d2) o (Map (fun z : RegularFunction (ball (m:=X)) => approximate z d1) s) (Map (fun z : RegularFunction (ball (m:=X)) => approximate z d1) s0) (Map (fun z : RegularFunction (ball (m:=X)) => approximate z d2) t) (Map (fun z : RegularFunction (ball (m:=X)) => approximate z d2) t0)). rewrite -> StepFSupBallGlueGlue in H. destruct H. split; revert d1 d2. exact (Hl H). exact (Hr H0). 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