proposition: Lemma Zpower_pos_powerRZ : forall n m, IZR (Z.pow_pos n m) = IZR n ^Z Zpos m.
proof: Proof. intros. rewrite Zpower_pos_nat; simpl. induction (Pos.to_nat m). - easy. - unfold Zpower_nat; simpl. rewrite mult_IZR. now rewrite <- IHn0. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac