proposition: Theorem Zpower_nat_Z_powerRZ : forall (n : Z) (m : nat), IZR (Zpower_nat n m) = powerRZ (IZR n) (Z_of_nat m).
proof: Proof. intros n m; elim m; simpl in |- *; auto with real. intros m1 H'; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; simpl in |- *. replace (Zpower_nat n (S m1)) with (n * Zpower_nat n m1)%Z. rewrite mult_IZR; auto with real. rewrite H'; simpl in |- *. case m1; simpl in |- *; auto with real. intros m2; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto. unfold Zpower_nat in |- *; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz