proposition: Lemma nth_derive_Rball_nth_derive_Rball': forall c r m n f g (pr : D_Rball c r n f) (pr' : D_Rball c r m g) (le: (n <= m)%nat), Rball_eq c r f g -> Rball_eq c r (nth_derive_Rball c r f pr) (nth_derive_Rball' c r n g pr' le).
proof: Proof. intro_all ; eapply nth_derive_Rball_ext ; eassumption. Qed.
imports: Reals Rfunction_classes Ranalysis_def Ranalysis_def_simpl Rfunction_def Rextensionality Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rinterval Nth_derivative_def