proposition: Theorem Zpower_nat_powerRZ_absolu : forall n m : Z, (0 <= m)%Z -> IZR (Zpower_nat n (Z.abs_nat m)) = powerRZ (IZR n) m.
proof: Proof. intros n m; case m; simpl in |- *; auto with zarith. intros p H'; elim (nat_of_P p); simpl in |- *; auto with zarith. intros n0 H'0; rewrite <- H'0; simpl in |- *; auto with zarith. rewrite <- mult_IZR; auto. intros p H'; contradict H'; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz