proposition: Theorem Bnearbyint_correct : forall md x, B2R (Bnearbyint md x) = round radix2 (FIX_exp 0) (round_mode md) (B2R x) /\ is_finite (Bnearbyint md x) = is_finite x /\ (is_nan (Bnearbyint md x) = false -> Bsign (Bnearbyint md x) = Bsign x).
proof: Proof. intros md. assert (round_0_ : 0%R = (round radix2 (FIX_exp 0) (round_mode md) 0)). { symmetry. apply round_0. apply valid_rnd_round_mode. } intros [sx | sx | | sx mx ex Hx]; try easy. unfold Bnearbyint. destruct Bnearbyint_correct_aux as [H1 [H2 [H3 H4]]]. repeat split. - rewrite B2R_SF2B. easy. - rewrite is_finite_SF2B. easy. - rewrite is_nan_SF2B. rewrite Bsign_SF2B. easy. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative