proposition: Lemma C_Rball_implies_D_Rball : forall n f c r, C_Rball c r n f -> D_Rball c r n f.
proof: Proof. intro n ; induction n ; intros f c r H. constructor. inversion H ; eapply Db_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