proposition: Lemma D_derive: forall n f (pr : derivable f), D (S n) f -> D n (derive f pr).
proof: Proof. intros n f pr Dnf ; inversion_clear Dnf ; eapply D_ext ; [| eassumption] ; intro ; eapply pr_nu. 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