proposition: Lemma powerRZ_mult m x y : (powerRZ (x*y) m = powerRZ x m * powerRZ y m)%R.
proof: Proof. destruct (intP m) as [ | | n Hm ]. - now simpl; rewrite Rmult_1_l. - now rewrite <- !pow_powerRZ, Rpow_mult_distr. - rewrite !powerRZ_neg', <- Rinv_mult. now rewrite <- !pow_powerRZ, Rpow_mult_distr. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac