proposition: Lemma powerRZ_mult_distr_depr : forall m x y, ((0 <= m)%Z \/ (x * y <> 0)%R) -> (powerRZ (x*y) m = powerRZ x m * powerRZ y m)%R.
proof: Proof. intros m x y _. apply powerRZ_mult. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac