proposition: Lemma derivable_pt_lim_pow_pos : forall (x:R) (n:nat), (0 < n)%nat -> derivable_pt_lim (fun y:R => y ^ n) x (INR n * x ^ pred n).
proof: Proof. intros. induction n as [| n Hrecn]. - elim (Nat.lt_irrefl _ H). - cut (n = 0%nat \/ (0 < n)%nat). + intro; elim H0; intro. * rewrite H1; simpl. replace (fun y:R => y * 1) with (id * fct_cte 1)%F by reflexivity. replace (1 * 1) with (1 * fct_cte 1 x + id x * 0). -- apply derivable_pt_lim_mult. ++ apply derivable_pt_lim_id. ++ apply derivable_pt_lim_const. -- unfold fct_cte, id; ring. * replace (fun y:R => y ^ S n) with (fun y:R => y * y ^ n) by reflexivity. replace (pred (S n)) with n; [ idtac | reflexivity ]. replace (fun y:R => y * y ^ n) with (id * (fun y:R => y ^ n))%F by reflexivity. set (f := fun y:R => y ^ n). replace (INR (S n) * x ^ n) with (1 * f x + id x * (INR n * x ^ pred n)). -- apply derivable_pt_lim_mult. { apply derivable_pt_lim_id. } unfold f; apply Hrecn; assumption. -- unfold f. pattern n at 1 5; replace n with (S (pred n)). { unfold id; rewrite S_INR; simpl. ring. } apply Nat.lt_succ_pred with 0%nat; assumption. + inversion H. * left; reflexivity. * right. apply Nat.lt_le_trans with 1%nat. -- apply Nat.lt_0_succ. -- assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv