proposition: Lemma derive_pt_eq_0 : forall f (x l:R) (pr:derivable_pt f x), derivable_pt_lim f x l -> derive_pt f x pr = l.
proof: Proof. intros; elim (derive_pt_eq f x l pr); intros. apply (H1 H). Qed.
imports: Rbase Rfunctions Rlimit Rderiv