proposition: Lemma Zpower_nat_powerRZ_absolu : forall n m:Z, (0 <= m)%Z -> IZR (Zpower_nat n (Z.abs_nat m)) = IZR n ^Z m.
proof: Proof. intros n m; case m; simpl; auto with zarith. - intros p H'; elim (Pos.to_nat p); simpl; auto with zarith. intros n0 H'0; rewrite <- H'0; simpl; auto with zarith. rewrite <- mult_IZR; auto. - intros p H'; absurd (0 <= Zneg p)%Z; auto with zarith. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac