proposition: Lemma nth_derive_Rball_ext : forall c r (n : nat) (f g : R -> R) (pr1 : D_Rball c r n f) (pr2 : D_Rball c r n g), Rball_eq c r f g -> Rball_eq c r (nth_derive_Rball c r f pr1) (nth_derive_Rball c r g pr2).
proof: Proof. intros c r n ; induction n ; intros f g pr1 pr2 Heq. apply Heq. apply IHn ; intros x x_in ; eapply derive_Rball_ext_strong ; eassumption. Qed.
imports: Reals Rfunction_classes Ranalysis_def Ranalysis_def_simpl Rfunction_def Rextensionality Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rinterval Nth_derivative_def