proposition: Lemma nth_derive'_ext : forall (f g : R -> R) (k m n : nat) (pr1 : D k f) (pr2 : D m g) (nlek : (n <= k)%nat) (nlem : (n <= m)%nat), f == g -> nth_derive' n f pr1 nlek == nth_derive' n g pr2 nlem.
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