proposition: Lemma D_Rball_plus: 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 c r n ; induction n ; intros f g Dnf Dng ; inversion_clear Dnf ; inversion_clear Dng. constructor. apply Db_S with (derivable_in_plus _ _ _ pr pr0) ; apply D_Rball_ext with (derive_Rball c r f pr + derive_Rball c r g pr0)%F. intros x x_in ; symmetry ; apply derive_Rball_plus ; assumption. 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