proposition: Theorem mag_le_Zpower : forall m e, m <> Z0 -> (Z.abs m < Zpower r e)%Z-> (mag (IZR m) <= e)%Z.
proof: Proof. intros m e Zm Hm. apply mag_le_bpow. now apply IZR_neq. destruct (Zle_or_lt 0 e). rewrite <- abs_IZR, <- IZR_Zpower with (1 := H). now apply IZR_lt. elim Zm. cut (Z.abs m < 0)%Z. now case m. clear -Hm H. now destruct e. Qed.
imports: Coq(Psatz Reals ZArith) Zaux