proposition: Lemma derivable_pt_lim_in_ext_strong: forall f g x (D : R -> Prop) l, D x -> (forall x, D x -> f x = g x) -> derivable_pt_lim_in D f x l -> derivable_pt_lim_in D g x l.
proof: Proof. intros f g x D l Dx Heq Hf eps eps_pos ; destruct (Hf _ eps_pos) as [alpha [alpha_pos Halpha]] ; exists alpha ; split ; [assumption |]. intros ; rewrite growth_rate_ext_strong with (g := f) (D := D). apply Halpha ; assumption. assumption. intros ; symmetry ; apply Heq ; assumption. destruct H as [[Dy _] _] ; exact Dy. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics