proposition: Lemma pr_nu : forall f (x:R) (pr1 pr2:derivable_pt f x), derive_pt f x pr1 = derive_pt f x pr2.
proof: Proof. intros f x (x0,H0) (x1,H1). apply (uniqueness_limite f x x0 x1 H0 H1). Qed.
imports: Rbase Rfunctions Rlimit Rderiv