proposition: Theorem IZR_Zpower_pos : forall n m, IZR (Zpower_pos n m) = powerRZ (IZR n) (Zpos m).
proof: Proof. intros. rewrite Zpower_pos_nat. simpl. induction (nat_of_P m). apply refl_equal. unfold Zpower_nat. simpl. rewrite mult_IZR. apply Rmult_eq_compat_l. exact IHn0. Qed.
imports: Coq(Psatz Reals ZArith) Zaux