proposition: Theorem INR_power : forall n m : nat, INR (power n m) = (INR n ^ m)%R.
proof: Proof. intros n m; elim m; simpl in |- *; auto with real. intros m1 H; rewrite mult_INR; rewrite H; auto. Qed.
imports: Coq(ZArith Classical_Prop) Coq(Rbase Rfunctions Ranalysis Rtrigo)