proposition: Theorem derivable_pt_lim_power : forall x y:R, 0 < x -> derivable_pt_lim (fun x => Rpower x y) x (y * Rpower x (y - 1)).
proof: Proof. intros x y H. unfold Rminus; rewrite Rpower_plus. rewrite Rpower_Ropp. rewrite Rpower_1; auto. rewrite <- Rmult_assoc. unfold Rpower. apply derivable_pt_lim_comp with (f1 := ln) (f2 := fun x => exp (y * x)). - apply derivable_pt_lim_ln; assumption. - rewrite (Rmult_comm y). apply derivable_pt_lim_comp with (f1 := fun x => y * x) (f2 := exp). + pattern y at 2; replace y with (0 * ln x + y * 1). * apply derivable_pt_lim_mult with (f1 := fun x:R => y) (f2 := fun x:R => x). -- apply derivable_pt_lim_const with (a := y). -- apply derivable_pt_lim_id. * ring. + apply derivable_pt_lim_exp. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra