proposition: Lemma D_Rball_infty_opp: forall c r f, D_Rball_infty c r f -> D_Rball_infty c r (- f)%F.
proof: Proof. intro_all ; apply D_Rball_opp ; eapply_assumption. Qed.
imports: Rbase Ranalysis Lia Lra Rfunctions Rfunction_facts Rextensionality Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rfunction_classes_def MyR_dist Reals.Tactics