proposition: Theorem binary_round_correct : forall m sx mx ex, let z := binary_round m sx mx ex in valid_binary z = true /\ let x := F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) in if Rlt_bool (Rabs (round radix2 fexp (round_mode m) x)) (bpow radix2 emax) then FF2R radix2 z = round radix2 fexp (round_mode m) x /\ is_finite_FF z = true /\ sign_FF z = sx else z = binary_overflow m sx.
proof: Proof. intros mode sx mx ex. generalize (binary_round_correct prec emax _ _ mode sx mx ex). simpl. unfold binary_round. destruct Rlt_bool. - now destruct BinarySingleNaN.binary_round. - intros [H1 ->]. split. rewrite valid_binary_SF2FF by apply is_nan_binary_overflow. now apply binary_overflow_correct. easy. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN