proposition: Theorem IZR_Zpower_nat : forall e : nat, IZR (Zpower_nat r e) = bpow (Z_of_nat e).
proof: Proof. intros [|e]. split. rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ. rewrite <- Zpower_pos_nat. now rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P. Qed.
imports: Coq(Psatz Reals ZArith) Zaux