proposition: Theorem Rpower_pow : forall (n : nat) (x : R), (0 < x)%R -> Rpower x (INR n) = (x ^ n)%R.
proof: Proof. intros n; elim n; simpl in |- *; auto; fold INR in |- *. intros x H; apply Rpower_O; auto. intros n1; case n1. intros H x H0; simpl in |- *; rewrite Rmult_1_r; apply Rpower_1; auto. intros n0 H x H0; rewrite Rpower_plus; rewrite H; try rewrite Rpower_1; auto with real. Qed.
imports: Coq(ZArith Classical_Prop) Coq(Rbase Rfunctions Ranalysis Rtrigo)