proposition: Lemma C_implies_D : forall n f, C n f -> D n f.
proof: Proof. intro n ; induction n ; intros f H. constructor. inversion H ; apply D_S with pr ; apply IHn ; assumption. 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