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