proposition: Lemma Zpower_nat_powerRZ : forall n m:nat, IZR (Zpower_nat (Z.of_nat n) m) = INR n ^Z Z.of_nat m.
proof: Proof. intros n m; elim m; simpl; auto with real. intros m1 H'; rewrite SuccNat2Pos.id_succ; simpl. replace (Zpower_nat (Z.of_nat n) (S m1)) with (Z.of_nat n * Zpower_nat (Z.of_nat n) m1)%Z. - rewrite mult_IZR; auto with real. repeat rewrite <- INR_IZR_INZ; simpl. rewrite H'; simpl. case m1; simpl; auto with real. intros m2; rewrite SuccNat2Pos.id_succ; auto. - unfold Zpower_nat; auto. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac