proposition: Lemma nested_balls (x1 x2 : Q) {y1 y2 : Q} {e : Qinf} : @ball _ (msp_mspc_ball Q_as_MetricSpace) e x1 x2 -> x1 ≤ y1 -> y1 ≤ y2 -> y2 ≤ x2 -> @ball _ (msp_mspc_ball Q_as_MetricSpace) e y1 y2.
proof: Proof. intros B A1 A2 A3. destruct e as [e |]; [| apply mspc_inf]. apply mspc_ball_Qabs_flip in B. apply mspc_ball_Qabs_flip. assert (x1 ≤ x2). now apply (PreOrder_Transitive _ y1); [|apply (PreOrder_Transitive _ y2)]. rewrite abs.abs_nonneg by now apply rings.flip_nonneg_minus. rewrite abs.abs_nonneg in B by now apply rings.flip_nonneg_minus. apply rings.flip_le_minus_l. apply rings.flip_le_minus_l in B. apply (PreOrder_Transitive _ x2); [easy|]. apply (PreOrder_Transitive _ (e + x1)); [easy|]. apply (orders.order_preserving (e +)); easy. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.metric2.Complete CoRN.metric2.Metric CoRN.ode.metric CoRN.model.totalorder.QposMinMax MathClasses.interfaces.abstract_algebra MathClasses.interfaces.rationals MathClasses.implementations.stdlib_rationals MathClasses.orders.orders MathClasses.orders.semirings MathClasses.orders.rings MathClasses.theory.rings CoRN.model.metric2.CRmetric CoRN.model.setoids.Qsetoid CoRN.model.metric2.Qmetric CoRN.reals.fast.CRArith CoRN.reals.fast.CRball CoRN.reals.fast.CRabs MathClasses.theory.abs MathClasses.orders.minmax