proposition: Theorem mag_unique_pos : forall (x : R) (e : Z), (bpow (e - 1) <= x < bpow e)%R -> mag x = e :> Z.
proof: Proof. intros x e1 He1. rewrite <- mag_abs. apply mag_unique. rewrite 2!Rabs_pos_eq. exact He1. apply Rle_trans with (2 := proj1 He1). apply bpow_ge_0. apply Rabs_pos. Qed.
imports: Coq(Psatz Reals ZArith) Zaux