proposition: Lemma derivable_pt_pow : forall (n:nat) (x:R), derivable_pt (fun y:R => y ^ n) x.
proof: Proof. intros; unfold derivable_pt. exists (INR n * x ^ pred n). apply derivable_pt_lim_pow. Qed.
imports: Rbase Rfunctions Rlimit Rderiv