proposition: Lemma derivable_pt_lim_in_plus: forall D f g x l1 l2, derivable_pt_lim_in D f x l1 -> derivable_pt_lim_in D g x l2 -> derivable_pt_lim_in D (f + g)%F x (l1 + l2).
proof: Proof. intros ; eapply limit1_ext. intros y Hy ; symmetry ; apply growth_rate_plus_compat ; split ; [unfold no_cond ; trivial | apply Hy]. apply limit_plus ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics