fact: Definition powerRZ (x:R) (n:Z) := match n with | Z0 => 1 | Zpos p => x ^ Pos.to_nat p | Zneg p => / x ^ Pos.to_nat p end.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac