proposition: Lemma D_infty_plus : forall f g, D_infty f -> D_infty g -> D_infty (f + g)%F.
proof: Proof. intros f g Df Dg n ; apply D_plus ; trivial. 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