proposition: Lemma mspc_ball_convex (x1 x2 r a x : Q) : @mspc_ball Q (msp_mspc_ball Q_as_MetricSpace) r a x1 -> @mspc_ball Q (msp_mspc_ball Q_as_MetricSpace) r a x2 -> x ∈ (x1, x2) -> @mspc_ball Q (msp_mspc_ball Q_as_MetricSpace) r a x.
proof: Proof. intros A1 A2 A3. rewrite mspc_ball_Qle in A1, A2. apply mspc_ball_Qle. destruct A1 as [A1' A1'']; destruct A2 as [A2' A2'']; destruct A3 as [A3' A3'']. split. + now transitivity (meet x1 x2); [apply meet_glb |]. + now transitivity (join x1 x2); [| apply join_lub]. 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