proposition: Lemma C_C_Rball: forall c r n f, C n f -> C_Rball c r n f.
proof: Proof. intros c r n ; induction n ; intros f Cnf ; inversion_clear Cnf. constructor ; apply continuity_continuity_in ; assumption. apply Cb_S with (derivable_derivable_in f (Rball c r) pr). eapply C_Rball_ext ; [| eapply IHn ; eassumption]. apply derive_derive_Rball. 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