proposition: Lemma int_lip (e M : Q) : (∀ x, @ball Q (msp_mspc_ball Q_as_MetricSpace) r a x -> abs (f x) ≤ 'M) -> @ball Q (msp_mspc_ball Q_as_MetricSpace) e x1 x2 -> @ball CR (msp_mspc_ball CR) (M * e) (F x1) (F x2).
proof: Proof. intros A1 A2. apply CRball.gball_CRabs. subst F; cbv beta. change (int f x0 x1 - int f x0 x2)%CR with (int f x0 x1 - int f x0 x2). pose proof (int_diff f x0 x1 x2). rewrite H1. change (abs (int f x2 x1) ≤ '(M * e)). transitivity ('(M * abs (x1 - x2))). + rewrite mult_comm. apply int_abs_bound; trivial. intros x A3; apply A1, (mspc_ball_convex x2 x1); easy. + apply CRle_Qle. assert (0 ≤ M). - apply CRle_Qle. transitivity (abs (f a)); [apply CRabs_nonneg | apply A1, @mspc_refl]. exact (msp_mspc_ball_ext Q_as_MetricSpace). easy. - change (M * abs (x1 - x2) ≤ M * e). apply (orders.order_preserving (M *.)). apply gball_Qabs, A2. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.reals.CRreal Coq.Unicode.Utf8 Coq.Program.Program CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.tactics.Qauto Coq.QArith.Qround CoRN.model.metric2.Qmetric CoRN.stdlib_omissions.P CoRN.stdlib_omissions.Z CoRN.stdlib_omissions.Q CoRN.stdlib_omissions.N CoRN.ode.metric CoRN.ode.FromMetric2 CoRN.ode.SimpleIntegration MathClasses.misc.propholds