proposition: Lemma nth_derive_Rball_1: forall c r f (pr : D_Rball c r 1 f) pr', nth_derive_Rball c r f pr == derive_Rball c r f pr'.
proof: Proof. intros ; eapply derive_Rball_ext ; reflexivity. Qed.
imports: Reals Rfunction_classes Ranalysis_def Ranalysis_def_simpl Rfunction_def Rextensionality Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rinterval Nth_derivative_def