proposition: Theorem is_nan_binary_round : forall mode sx mx ex, is_nan_SF (binary_round mode sx mx ex) = false.
proof: Proof. intros mode sx mx ex. generalize (binary_round_correct mode sx mx ex). simpl. destruct binary_round ; try easy. intros [_ H]. destruct Rlt_bool ; try easy. unfold binary_overflow in H. now destruct overflow_to_inf. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative