proposition: Lemma eq_binary_overflow_FF2SF : forall x m s, FF2SF x = BinarySingleNaN.binary_overflow prec emax m s -> x = binary_overflow m s.
proof: Proof. intros x m s H. unfold binary_overflow. rewrite <- H. apply eq_sym, SF2FF_FF2SF. rewrite <- is_nan_FF2SF, H. apply is_nan_binary_overflow. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN