proposition: Theorem mag_ge_bpow : forall x e, (bpow (e - 1) <= Rabs x)%R -> (e <= mag x)%Z.
proof: Proof. intros x e H. destruct (Rlt_or_le (Rabs x) (bpow e)) as [Hxe|Hxe]. - assert (mag x = e :> Z) as Hln. now apply mag_unique; split. rewrite Hln. now apply Z.le_refl. - apply Zlt_le_weak. now apply mag_gt_bpow. Qed.
imports: Coq(Psatz Reals ZArith) Zaux