proposition: Lemma integral_uc_prf : @is_UniformlyContinuousFunction L1StepQ Q_as_MetricSpace IntegralQ Qpos2QposInf.
proof: Proof. intros e x y. simpl in *. rewrite -> Qball_Qabs. rewrite -> Integral_minus. unfold L1Ball, L1Distance. generalize (x - y). clear x y. intros x. intros Hx. eapply Qle_trans. apply Abs_Integral_Norm. assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.structures.StepQsec CoRN.metric2.UniformContinuity CoRN.metric2.Prelength 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