proposition: Lemma lipschitz_bounded (a r M x : Q) : abs (f a) ≤ 'M -> @ball Q (msp_mspc_ball Q_as_MetricSpace) r a x -> abs (f x) ≤ '(M + L a r * r).
proof: Proof. intros A1 A2. assert (f x = f x - 0) as H1. { rewrite rings.minus_0_r. reflexivity. } pose proof (CRabs_wd _ _ H1). rewrite H2. clear H2 H1. apply mspc_ball_CRabs, mspc_symm. apply (mspc_triangle _ _ _ (f a)). - apply mspc_ball_CRabs. assert (0 - f a = - f a) as H1. { rewrite rings.plus_0_l. reflexivity. } pose proof (CRabs_wd _ _ H1). rewrite H2. clear H2 H1. pose proof (CRabs_negate (f a)). now rewrite H1. - apply (@llip _ _ _ _ (msp_mspc_ball_ext Q_as_MetricSpace) f _ H). 2: exact A2. 2: exact A2. apply mspc_refl. apply (@radius_nonneg _ _ (msp_mspc_ball_ext Q_as_MetricSpace) a x). exact 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