proposition: Lemma derivable_pt_lim_in_ext: forall f g x D l, f == g -> derivable_pt_lim_in D f x l -> derivable_pt_lim_in D g x l.
proof: Proof. intros f g x D l Heq Hf eps eps_pos ; destruct (Hf _ eps_pos) as [alpha [alpha_pos Halpha]] ; exists alpha ; split ; [assumption |]. intros ; erewrite growth_rate_ext ; [eapply Halpha | symmetry] ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics