proposition: Theorem mag_round : forall rnd {Hrnd : Valid_rnd rnd} x, (round rnd x <> 0)%R -> (mag beta (round rnd x) = mag beta x :> Z) \/ Rabs (round rnd x) = bpow (Z.max (mag beta x) (fexp (mag beta x))).
proof: Proof. Proof with auto with typeclass_instances. intros rnd Hrnd x. destruct (round_ZR_or_AW rnd x) as [Hr|Hr] ; rewrite Hr ; clear Hr rnd Hrnd. left. now apply mag_round_ZR. intros Zr. destruct (Req_dec x 0) as [Zx|Zx]. rewrite Zx, round_0... destruct (mag beta x) as (ex, Ex) ; simpl. specialize (Ex Zx). rewrite <- mag_abs. rewrite <- round_AW_abs. destruct (Zle_or_lt ex (fexp ex)) as [He|He]. right. rewrite Z.max_r with (1 := He). rewrite round_AW_UP with (1 := Rabs_pos _). now apply round_UP_small_pos. destruct (round_bounded_large_pos Zaway _ ex He Ex) as (H1,[H2|H2]). left. apply mag_unique. rewrite <- round_AW_abs, Rabs_Rabsolu. now split. right. now rewrite Z.max_l with (1 := Zlt_le_weak _ _ He). Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop