proposition: Lemma derivable_pt_lim_derivable_pt_lim_in: forall f D x l, derivable_pt_lim f x l -> derivable_pt_lim_in D f x l.
proof: Proof. intros f D x l Hl eps eps_pos ; destruct (Hl _ eps_pos) as [delta Hdelta] ; exists delta ; split. apply delta. intros y [[Dy xny] xy_bd] ; simpl ; unfold R_dist, growth_rate ; replace (f y) with (f (x + (y - x))) by (f_equal ; ring) ; apply Hdelta. intro Hf ; apply xny ; revert Hf ; clear ; intuition (auto with real). apply xy_bd. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics