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