proposition: Lemma powerRZ_Rpower x z : (0 < x)%R -> powerRZ x z = Rpower x (IZR z).
proof: Proof. intros Hx. destruct (intP z). - now rewrite Rpower_O. - rewrite <- pow_powerRZ, <- Rpower_pow by assumption. now rewrite INR_IZR_INZ. - rewrite opp_IZR, Rpower_Ropp. rewrite powerRZ_neg'. now rewrite <- pow_powerRZ, <- INR_IZR_INZ, Rpower_pow. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra