proposition: Theorem powerRZ_Zopp : forall (e : R) (z : Z), e <> 0%R -> powerRZ e (- z) = (/ powerRZ e z)%R.
proof: Proof. intros e z H. rewrite powerRZ_neg by easy. now apply powerRZ_inv. Qed.
imports: Reals ZArith List PeanoNat Psatz