proposition: Lemma derivable_derive : forall f (x:R) (pr:derivable_pt f x), exists l : R, derive_pt f x pr = l.
proof: Proof. intros; exists (proj1_sig pr). unfold derive_pt; reflexivity. Qed.
imports: Rbase Rfunctions Rlimit Rderiv