proposition: Theorem Bnearbyint_correct : forall nearbyint_nan md x, B2R (Bnearbyint nearbyint_nan md x) = round radix2 (FIX_exp 0) (round_mode md) (B2R x) /\ is_finite (Bnearbyint nearbyint_nan md x) = is_finite x /\ (is_nan (Bnearbyint nearbyint_nan md x) = false -> Bsign (Bnearbyint nearbyint_nan md x) = Bsign x).
proof: Proof. intros nearbyint_nan mode x. generalize (Bnearbyint_correct prec emax _ mode (B2BSN x)). replace (BinarySingleNaN.Bnearbyint _ _) with (B2BSN (Bnearbyint nearbyint_nan mode x)) by apply B2BSN_BSN2B. intros H. destruct x as [sx|[|]|sx plx Hplx|sx mx ex Hx] ; try easy. now destruct Bnearbyint. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN