proposition: Theorem round_FIX_IZR : forall f x, round radix2 (FIX_exp 0) f x = IZR (f x).
proof: Proof. intros f x. unfold round, F2R. simpl. rewrite Rmult_1_r. apply f_equal. apply f_equal. unfold scaled_mantissa. simpl. apply Rmult_1_r. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Ulp Round_NE