proposition: Lemma C_Rball_plus: forall c r n f g, C_Rball c r n f -> C_Rball c r n g -> C_Rball c r n (f + g)%F.
proof: Proof. intros c r n ; induction n ; intros f g Cnf Cng ; inversion_clear Cnf ; inversion_clear Cng. constructor ; intros x x_in ; apply limit_plus ; eapply_assumption ; assumption. apply Cb_S with (derivable_in_plus _ _ _ pr pr0) ; apply C_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