proposition: Lemma D_Rball_minus: forall c r n f g, D_Rball c r n f -> D_Rball c r n g -> D_Rball c r n (f - g)%F.
proof: Proof. intros ; unfold minus_fct, Rminus ; apply D_Rball_plus ; [| apply D_Rball_opp] ; 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