proposition: Lemma D_Rball_S_implies_C_Rball : forall c r n f, D_Rball c r (S n) f -> C_Rball c r n f.
proof: Proof. intros c r n ; induction n ; intros f Hf ; inversion Hf. constructor ; apply derivable_in_continuity_in ; assumption. apply Cb_S with pr ; 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