proposition: Theorem is_nan_binary_overflow : forall mode s, is_nan_SF (binary_overflow mode s) = false.
proof: Proof. intros mode s. unfold binary_overflow. now destruct overflow_to_inf. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative