proposition: Lemma pow_powerRZ (r : R) (n : nat) : (r ^ n)%R = powerRZ r (Z_of_nat n).
proof: Proof. induction n; [easy|simpl]. now rewrite SuccNat2Pos.id_succ. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac