proposition: Lemma derive_pt_eq : forall f (x l:R) (pr:derivable_pt f x), derive_pt f x pr = l <-> derivable_pt_lim f x l.
proof: Proof. intros; split. - intro; assert (H1 := proj2_sig pr); unfold derive_pt in H; rewrite H in H1; assumption. - intro; assert (H1 := proj2_sig pr); unfold derivable_pt_abs in H1. assert (H2 := uniqueness_limite _ _ _ _ H H1). unfold derive_pt; unfold derivable_pt_abs. symmetry ; assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv