proposition: Lemma D_Rball_opp: forall c r n f, D_Rball c r n f -> D_Rball c r n (- f)%F.
proof: Proof. intros c r n ; induction n ; intros f Hf ; inversion_clear Hf. constructor. apply Db_S with (derivable_in_opp _ _ pr) ; apply D_Rball_ext with (- derive_Rball c r f pr)%F. symmetry ; apply Req_Rball_eq ; intro ; apply derive_Rball_opp. apply IHn ; 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