proposition: Lemma derive_pt_Rball_plus: forall f g c r x prf prg prfg, Rball c r x -> derive_pt_in (Rball c r) (f + g)%F x prfg = derive_pt_in (Rball c r) f x prf + derive_pt_in (Rball c r) g x prg.
proof: Proof. intros f g c r x [] [] [] x_in ; eapply derivable_pt_lim_Rball_uniqueness, derivable_pt_lim_in_plus ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics