proposition: Lemma nth_derive_nth_derive': forall m n f g (pr : D n f) (pr' : D m g) (le: (n <= m)%nat), f == g -> nth_derive f pr == nth_derive' n g pr' le.
proof: Proof. intros ; apply nth_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