proposition: Lemma extend_inside : ∀ {Y : CProp} {H : MetricSpaceBall Y} { _ : @ExtMetricSpaceClass Y H }, ∀ (a x : Q) (r : QnonNeg), @ball Q (msp_mspc_ball Q_as_MetricSpace) (proj1_sig r) a x → ∃ p : @ball Q (msp_mspc_ball Q_as_MetricSpace) (proj1_sig r) a x, ∀ f : sig (fun x : Q => @ball Q (msp_mspc_ball Q_as_MetricSpace) (proj1_sig r) a x) → Y, @extend Y a r f x = f (x ↾ p).
proof: Proof. intros Y H H0 a x r A. apply mspc_ball_Qle in A. destruct A as [A1 A2]. unfold extend. destruct (decide (x < a - proj1_sig r)) as [H1 | H1]. * apply orders.lt_not_le_flip in H1; elim (H1 A1). * destruct (decide (a + proj1_sig r < x)) as [H2 | H2]. + apply orders.lt_not_le_flip in H2; elim (H2 A2). + eexists; intro f; reflexivity. 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.ode.metric CoRN.ode.FromMetric2 CoRN.ode.AbstractIntegration CoRN.ode.SimpleIntegration CoRN.ode.BanachFixpoint MathClasses.interfaces.canonical_names MathClasses.misc.decision MathClasses.misc.setoid_tactics MathClasses.misc.util MathClasses.implementations.stdlib_rationals MathClasses.theory.rationals