proposition: Lemma derivable_pt_derivable_pt_in: forall f D x, derivable_pt f x -> derivable_pt_in D f x.
proof: Proof. intros f D x [l Hl] ; exists l ; apply derivable_pt_lim_derivable_pt_lim_in ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics