proposition: Lemma derivable_pt_lim_pow : forall (x:R) (n:nat), derivable_pt_lim (fun y:R => y ^ n) x (INR n * x ^ pred n).
proof: Proof. intros. induction n as [| n Hrecn]. - simpl. rewrite Rmult_0_l. replace (fun _:R => 1) with (fct_cte 1); [ apply derivable_pt_lim_const | reflexivity ]. - apply derivable_pt_lim_pow_pos. apply Nat.lt_0_succ. Qed.
imports: Rbase Rfunctions Rlimit Rderiv