proposition: Lemma sup_uc_prf : @is_UniformlyContinuousFunction LinfStepQ Q_as_MetricSpace (StepQSup:LinfStepQ -> Q) Qpos2QposInf.
proof: Proof. intros e x y. simpl. rewrite -> Qball_Qabs. revert x y. apply: StepF_ind2. intros s s0 t t0 Hs Ht. simpl. intros H H1. rewrite <- Hs, <- Ht in H1. specialize (H H1). refine (Qle_trans _ _ _ _ H). rewrite <- (StepQSup_wd s s0). rewrite <- (StepQSup_wd t t0). apply Qle_refl. apply StepF_eq_change_base_setoid, Ht. apply StepF_eq_change_base_setoid, Hs. intros x y. rewrite <- Qball_Qabs. auto. intros o s s0 t t0 H0 H1 H2. simpl in *. rewrite StepQSup_glue, StepQSup_glue. assert (X:forall a b, (-(a-b)==b-a)%Q). intros; ring. unfold StepFSupBall in H2. revert H2. rewrite (GlueAp (ballS Q_as_MetricSpace (proj1_sig e) ^@> glue o s s0)). rewrite (GlueAp (constStepF (ballS Q_as_MetricSpace (proj1_sig e)))). rewrite SplitLGlue, SplitRGlue. intros [H2a H2b]. apply Qabs_case; intros H; [|rewrite <- Qabs_opp in H0, H1; rewrite -> X in *]; (rewrite -> Qmax_minus_distr_l; unfold Qminus; apply Qmax_lub;[|clear H0; rename H1 into H0]; (eapply Qle_trans;[|apply H0; auto]); (eapply Qle_trans;[|apply Qle_Qabs]); unfold Qminus; apply: plus_resp_leEq_lft; simpl; auto with * ). 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