proposition: Lemma derive_pt_derivable_pt_lim_interval: forall f lb ub x l (pr : derivable_pt_in (interval lb ub) f x), lb < ub -> interval lb ub x -> derive_pt_in (interval lb ub) f x pr = l -> derivable_pt_lim_in (interval lb ub) f x l.
proof: Proof. intros f lb ub x l [l' Hl'] Hlt x_in Hl ; subst ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics