proposition: Theorem mag_gt_Zpower : forall m e, m <> Z0 -> (Zpower r e <= Z.abs m)%Z -> (e < mag (IZR m))%Z.
proof: Proof. intros m e Zm Hm. apply mag_gt_bpow. rewrite <- abs_IZR. destruct (Zle_or_lt 0 e). rewrite <- IZR_Zpower with (1 := H). now apply IZR_le. apply Rle_trans with (bpow 0). apply bpow_le. now apply Zlt_le_weak. apply IZR_le. clear -Zm. lia. Qed.
imports: Coq(Psatz Reals ZArith) Zaux