proposition: Lemma derivable_nth_derive_Rball : forall c r n f (pr : derivable_Rball c r f) (pr1 : D_Rball c r (S n) f) (pr2 : D_Rball c r n (derive_Rball c r f pr)) l x, Rball c r x -> nth_derive_Rball c r (derive_Rball c r f pr) pr2 x = l -> nth_derive_Rball c r f pr1 x = l.
proof: Proof. intros c r n f pr pr1 pr2 l x Hl x_in. simpl. rewrite nth_derive_Rball_ext with (g := derive_Rball c r f pr) (pr2 := pr2). assumption. apply Req_Rball_eq, derive_Rball_ext_strong ; reflexivity. assumption. Qed.
imports: Reals Rfunction_classes Ranalysis_def Ranalysis_def_simpl Rfunction_def Rextensionality Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rinterval Nth_derivative_def