proposition: Theorem mag_le_bpow : forall x e, x <> 0%R -> (Rabs x < bpow e)%R -> (mag x <= e)%Z.
proof: Proof. intros x e Zx Hx. destruct (mag x) as (ex, Ex) ; simpl. specialize (Ex Zx). apply bpow_lt_bpow. now apply Rle_lt_trans with (Rabs x). Qed.
imports: Coq(Psatz Reals ZArith) Zaux