proposition: Lemma mspc_ball_edge_l : @ball Q (msp_mspc_ball Q_as_MetricSpace) (proj1_sig r) a (a - `r).
proof: Proof. destruct r as [e ?]; simpl. apply gball_Qabs. mc_setoid_replace (a - (a - e)) with e by ring. change (abs e ≤ e). rewrite abs.abs_nonneg; [reflexivity | trivial]. 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