proposition: Lemma derivable_pt_lim_ext : forall f g x l, (forall z, f z = g z) -> derivable_pt_lim f x l -> derivable_pt_lim g x l.
proof: Proof. intros f g x l fg df e ep; destruct (df e ep) as [d pd]; exists d; intros h; rewrite <- !fg; apply pd. Qed.
imports: Rbase Rfunctions Rlimit Rderiv