proposition: Lemma luc_gball (a w delta eps x y : Q) : 0 < eps -> (delta <= lmu a w eps)%Qinf -> @ball Q_as_MetricSpace w a x -> @ball Q_as_MetricSpace w a y -> @ball Q_as_MetricSpace delta x y -> ball eps (f x) (f y).
proof: Proof. intros A A1 A2 A3 A4. destruct (@luc_prf Q (msp_mspc_ball Q_as_MetricSpace) CR (msp_mspc_ball CR) f lmu L a w) as [_ H]. change (f x) with (@restrict Q (msp_mspc_ball Q_as_MetricSpace) CR f a w (exist _ _ A2)). change (f y) with (@restrict Q (msp_mspc_ball Q_as_MetricSpace) CR f a w (exist _ _ A3)). apply H; [apply A |]. destruct (lmu a w eps) as [q |] eqn:A5; [| easy]. apply (@mspc_monotone _ _ (@sig_mspc Q (msp_mspc_ball Q_as_MetricSpace) (msp_mspc_ball_ext Q_as_MetricSpace) (@mspc_ball Q (msp_mspc_ball Q_as_MetricSpace) w a) ) delta). apply A1. apply A4. 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