proposition: Lemma D_plus: forall n f g, D n f -> D n g -> D n (f + g)%F.
proof: Proof. intro n ; induction n ; intros f g Dnf Dng ; inversion_clear Dnf ; inversion_clear Dng. constructor. apply D_S with (derivable_plus _ _ pr pr0) ; apply D_ext with (plus_fct (derive f pr) (derive g pr0)). intro x ; symmetry ; transitivity (derive f pr x + derive g pr0 x). unfold derive ; rewrite derive_pt_eq ; apply derivable_pt_lim_plus ; eapply derive_pt_eq_1 ; reflexivity. auto. 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