proposition: Theorem mag_round_ZR : forall x, (round Ztrunc x <> 0)%R -> (mag beta (round Ztrunc x) = mag beta x :> Z).
proof: Proof. Proof with auto with typeclass_instances. intros x Zr. destruct (Req_dec x 0) as [Zx|Zx]. rewrite Zx, round_0... apply mag_unique. destruct (mag beta x) as (ex, Ex) ; simpl. specialize (Ex Zx). rewrite <- round_ZR_abs. split. apply round_large_pos_ge_bpow... rewrite round_ZR_abs. now apply Rabs_pos_lt. apply Ex. apply Rle_lt_trans with (2 := proj2 Ex). rewrite round_ZR_DN. apply round_DN_pt. apply Rabs_pos. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop