fact: Definition nth_derive_Rball' {m : nat} c r n f (pr: D_Rball c r m f) (nlem: (n <= m)%nat) : R -> R := nth_derive_Rball c r f (D_Rball_le _ _ _ _ _ nlem pr).
imports: Reals Rfunction_classes Ranalysis_def Ranalysis_facts