proposition: Lemma nth_derive_ext : forall (n : nat) (f g : R -> R) (pr1 : D n f) (pr2 : D n g), f == g -> nth_derive f pr1 == nth_derive g pr2.
proof: Proof. intro n ; induction n ; intros ; simpl ; [| apply IHn ; apply derive_ext] ; assumption. Qed.
imports: Reals Rfunction_classes Ranalysis_def Ranalysis_def_simpl Rfunction_def Rextensionality Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rinterval Nth_derivative_def