proposition: Lemma derivable_nth_derive : forall n f (pr : derivable f) (pr1 : D (S n) f) (pr2 : D n (derive f pr)) l x, nth_derive (derive f pr) pr2 x = l -> nth_derive f pr1 x = l.
proof: Proof. intros n f pr pr1 pr2 l x Hl. simpl. rewrite nth_derive_ext with (g := derive f pr) (pr2 := pr2). assumption. intro ; unfold derive ; apply pr_nu_var ; reflexivity. Qed.
imports: Reals Rfunction_classes Ranalysis_def Ranalysis_def_simpl Rfunction_def Rextensionality Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rinterval Nth_derivative_def