proposition: Theorem Rpower_pow : forall (n:nat) (x:R), 0 < x -> Rpower x (INR n) = x ^ n.
proof: Proof. intros n; elim n; simpl; auto; fold INR. - intros x H; apply Rpower_O; auto. - intros n1; case n1. + intros H x H0; simpl; rewrite Rmult_1_r; apply Rpower_1; auto. + intros n0 H x H0; rewrite Rpower_plus; rewrite H; try rewrite Rpower_1; try apply Rmult_comm || assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra