proposition: Lemma pr_nu_xeq : forall f (x1 x2:R) (pr1:derivable_pt f x1) (pr2:derivable_pt f x2), x1 = x2 -> derive_pt f x1 pr1 = derive_pt f x2 pr2.
proof: Proof. intros f x1 x2 H1 H2 Heq. subst. apply pr_nu. Qed.
imports: Rbase Rfunctions Rlimit Rderiv