proposition: Lemma derivable_in_plus: forall D f g, derivable_in D f -> derivable_in D g -> derivable_in D (f + g)%F.
proof: Proof. intros D f g Hf Hg x x_in ; eapply derivable_pt_in_plus ; [eapply Hf | eapply Hg] ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics