proposition: Lemma C_Rball_derive: forall c r n f pr, C_Rball c r (S n) f -> C_Rball c r n (derive_Rball c r f pr).
proof: Proof. intros c r n f pr Cnf ; inversion_clear Cnf ; eapply C_Rball_ext ; [| eassumption] ; eapply Req_Rball_eq, derive_Rball_ext ; reflexivity. Qed.
imports: Rbase Ranalysis Lia Lra Rfunctions Rfunction_facts Rextensionality Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rfunction_classes_def MyR_dist Reals.Tactics