proposition: Lemma nth_derive_Rball'_PI: forall c r m n f (pr1: D_Rball c r m f) (pr2: D_Rball c r m f) (le1 le2: (n <= m)%nat), Rball_eq c r (nth_derive_Rball' c r n f pr1 le1) (nth_derive_Rball' c r n f pr2 le2).
proof: Proof. intros ; apply nth_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