proposition: Theorem mag_unique : forall (x : R) (e : Z), (bpow (e - 1) <= Rabs x < bpow e)%R -> mag x = e :> Z.
proof: Proof. intros x e1 He. destruct (Req_dec x 0) as [Hx|Hx]. elim Rle_not_lt with (1 := proj1 He). rewrite Hx, Rabs_R0. apply bpow_gt_0. destruct (mag x) as (e2, Hx2). simpl. apply bpow_unique with (2 := He). now apply Hx2. Qed.
imports: Coq(Psatz Reals ZArith) Zaux