proposition: Lemma powerRZ_neg' x : forall alpha, powerRZ x (- alpha) = Rinv (powerRZ x alpha).
proof: Proof. intros [|n|n] ; simpl. - apply eq_sym, Rinv_1. - easy. - now rewrite Rinv_inv. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac