proposition: Lemma mspc_ball_weak_le (q q': Qinf): (q <= q')%Qinf → ∀ x y: X, mspc_ball q x y → mspc_ball q' x y.
proof: Proof. Proof with auto. destruct q, q'; simpl; intros... assert (q0 == q + (q0 - q))%Q as E by ring. rewrite (mspc_ball_proper q0 (q+(q0-q)) x y E). change (mspc_ball (Qinf.finite q + Qinf.finite (q0 - q)%Q) x y). apply mspc_triangle with y... apply mspc_refl. simpl. apply QArith_base.Qplus_le_r with q. ring_simplify... apply mspc_ball_inf. intuition. Qed.
imports: CoRN.algebra.RSetoid Arith List CoRN.model.totalorder.QposMinMax CSetoids Qmetric Qring Qinf QnnInf QnonNeg ProductMetric QposInf Qposclasses UniformContinuity MathClasses.implementations.stdlib_rationals stdlib_omissions.Pair stdlib_omissions.Q PointFree MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.theory.products